 Solution

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

The continuation receives both the computed value and the current computer memory. Therefore return invokes it with unchanged computer memory, while sequencing installs a continuation that passes the produced value and updated computer memory to the next computation:

result :: a -> M a
result x k s = k x s

bind :: M a -> (a -> M b) -> M b
bind p f k s = p (\x s' -> f x k s') s

For left identity, expand the two definitions:

(result (x) ▹ f) k s = (λ y t . f (y) k t) x s = f (x) k s .

For right identity,

(p ▹ result) k s = p (λ x t . result (x) k t) s = p (λ x t . k x t) s = p k s .

For associativity, both groupings reduce to the same expression:

((p ▹ f) ▹ g) k s (p ▹ (λ x . f (x) ▹ g)) k s = p (λ x t . f (x) (λ y u . g (y) k u) t) s, = p (λ x t . f (x) (λ y u . g (y) k u) t) s .

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

 New to topics? Read the docs here!