Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 1 / b

Table of contents
- Solution 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

to

p

, its output

t

to

f

, and the output

u

of

f

to

g

. By function extensionality,

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

 Ancestors (10)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (0)

There are currently no matching articles.

  See all articles in the same topic Create my own version