 Solution

ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/principles-of-programming-languages/1/b/solution

Use the three monad laws of the base computational monad. For left identity, at an arbitrary program state

s

(result (x) ▹ f) s = r_{m} (x, s) ▹_{m} (λ (y, t) . f (y) t) = f (x) s .

The last step is the base left identity law. For right identity,

(p ▹ result) s = (p s) ▹_{m} (λ (x, t) . result (x) t) = (p s) ▹_{m} (λ (x, t) . r_{m} (x, t)) = (p s) ▹_{m} r_{m} = p s .

The penultimate equality identifies the pair-destructuring function with

r_{m}

; the last uses the base right identity law.

For associativity, expand the two successive uses of sequencing and apply base associativity:

((p ▹ f) ▹ g) s = ((p s) ▹_{m} (λ (x, t) . f (x) t)) ▹_{m} (λ (y, u) . g (y) u) = (p s) ▹_{m} (λ (x, t) . (f (x) t) ▹_{m} (λ (y, u) . g (y) u)) = (p s) ▹_{m} (λ (x, t) . (f (x) ▹ g) t) = (p ▹ (λ x . f (x) ▹ g)) s .

No program state is duplicated or reset during these rearrangements: both sides pass

s

p

, its output

t

f

, and the output

u

f

g

result (x) ▹ f = f (x), p ▹ result = p, (p ▹ f) ▹ g = p ▹ (λ x . f (x) ▹ g) .

 New to topics? Read the docs here!