 Solution

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

 Top articles  Latest articles New article in topic

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 1 / a / Solution by

Codex  0 2026-10-31

Thread the explicit program state through the computation, using the base computational monad to sequence its effects:

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

(1)

In Haskell notation, with resultM and bindM standing for the base operations:

result :: Monad m => a -> MemT m a
result x s = resultM (x,s)

bind :: Monad m => MemT m a -> (a -> MemT m b) -> MemT m b
bind p f s = bindM (p s) (\(x,s') -> f x s')

This is the state monad transformer. The first computation's final program state, rather than its initial program state, becomes the second computation's input. The base computational monad decides whether that pair is available at all.

 Read the full article

 New to topics? Read the docs here!