Thread the explicit program state through the computation, using the base computational monad to sequence its effects:
(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.
Use the three monad laws of the base computational monad. For left identity, at an arbitrary program state ,
(1)
The last step is the base left identity law. For right identity,
(2)
The penultimate equality identifies the pair-destructuring function with ; the last uses the base right identity law.
For associativity, expand the two successive uses of sequencing and apply base associativity:
(3)
No program state is duplicated or reset during these rearrangements: both sides pass to , its output to , and the output of to . By function extensionality,
(4)
Reading preserves the computer memory; writing returns the unit type value; allocating returns both the fresh memory location and the allocator's updated computer memory:
get :: Monad m => Location -> MemT m Value
get a s = resultM (contents s a,s)

put :: Monad m => Location -> Value -> MemT m ()
put a v s = resultM ((),update s a v)

new :: Monad m => MemT m Location
new s = resultM (fresh s)
These use the memory interface in [ref]. In particular, fresh already returns its outputs in the order required by the state monad transformer:
(1)
There is one undifferentiated exception, so use the two alternatives of the Haskell algebraic data type Maybe: Just x succeeds and Nothing fails. A suitable exception monad transformer is:
type ExT m a = m (Maybe a)

result :: Monad m => a -> ExT m a
result x = resultM (Just x)

bind :: Monad m => ExT m a -> (a -> ExT m b) -> ExT m b
bind p f = bindM p (\r -> case r of
  Nothing -> resultM Nothing
  Just x  -> f x)

orelse :: Monad m => ExT m a -> ExT m a -> ExT m a
orelse p q = bindM p (\r -> case r of
  Nothing -> q
  Just x  -> resultM (Just x))

failure :: Monad m => ExT m a
failure = resultM Nothing
The distinction between bindM and bind matters. The handler must inspect the failed alternative using the base computational monad; the transformed bind would propagate failure without running that inspection. The alternative computation q runs only after p returns Nothing; any effects already performed by the base computational monad remain subject to that base's semantics.
Left identity follows by selecting Just x. Right identity follows because either alternative is passed back to resultM. For associativity, base associativity exposes the first alternative: Nothing propagates through both remaining steps; Just x runs f x, with its Nothing and Just alternatives treated identically on both sides. Thus this representation also satisfies the monad laws.
(1)
The identity monad embeds a value unchanged and sequences by ordinary application:
type IdM a = a
result :: a -> IdM a
result x = x
bind :: IdM a -> (a -> IdM b) -> IdM b
bind x f = f x
All three monad laws reduce to substitution in function application. There is no additional program state, failure alternative or continuation layer:
(1)
Expand the two type synonyms to see what survives an exception:
(1)
In the first order, a failed computation can still produce (Nothing,s'). The exception handler therefore runs with , including writes made before failure. In the second order, failure produces Nothing, with no returned computer memory. A handler defined by applying the underlying orelse pointwise runs its alternative from the original input computer memory . This gives rollback of this explicit program state for the failed branch.
For example, start with a memory location holding , write , fail, and handle the failure by reading that memory location. The first order returns ; the second returns . This rollback concerns the explicit computer memory only: arbitrary effects in the base computational monad are not thereby reversed.
(2)
A conventional programming language normally retains writes made before an exception is caught. Its mutable computer memory and exception handling therefore correspond more closely to .
Fix an answer type and let the continuation return its answer inside the base computational monad:
type ContT m a = (a -> m Answer) -> m Answer

result :: Monad m => a -> ContT m a
result x k = k x

bind :: Monad m => ContT m a -> (a -> ContT m b) -> ContT m b
bind p f k = p (\x -> f x k)
The continuation monad transformer changes the continuation supplied to p: it first runs f on the produced value, then uses the original final continuation k. Base sequencing is unnecessary in these two definitions because p already accepts a continuation returning m Answer. The customary lift, if desired, is lift q k = bindM q k.
(1)

Ancestors (9)

  1. Principles of programming languages
  2. 2015
  3. Past exam of the computer science course of the University of Oxford
  4. Computer science course of the University of Oxford
  5. Undergraduate course of the University of Oxford
  6. Course of the University of Oxford
  7. University of Oxford
  8. List of universities
  9. Home

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