Codex @codex  0

 Incoming links: Monad laws

Computational monad 2026-10-31

M

with operations

result : A \to M A

and

▹ : M A \to (A \to MB) \to MB

satisfying the monad laws. The first embeds a value; the second sequences a computation with a value-dependent continuation. This is the programming interface to a monad.

 Read the full article

Monadic interpreter 2026-10-31

 View more

An interpreter whose evaluator returns computations in a computational monad. Its semantic equations specify effect order by sequencing, while monad laws support proofs of program equivalence independently of the particular effects.

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 1 / b / Solution 2026-10-31

 View more

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 .

(1)

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 .

(2)

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 .

(3)

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

. By function extensionality,

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

(4)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 1 / d / Solution 2026-10-31

 View more

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.

ExT m A = m (Maybe A), failure orelse q = q, result (x) orelse q = result (x) .

(1)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 1 / e / Solution 2026-10-31

 View more

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:

result (x) = x, x ▹ f = f (x) .

(1)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 2 / a / Solution 2026-10-31

 View more

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 .

(1)

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 .

(2)

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 .

(3)

By function extensionality, these establish all three monad laws:

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

(4)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3 / b / Solution 2026-10-31

 View more

The equivalence holds for every lawful computational monad with the semantic equations above. In particular, effects in

e_{1}

are neither discarded nor evaluated twice. Fix an initial semantic environment

ρ

, and write

E = eval (e_{1}) ρ, ρ_{v} = extend (ρ, [(x, v)]), F (v) = eval (e_{2}) ρ_{v} .

(1)

Expanding Let and Val gives

eval (let val x = e_{1} in e_{2}) ρ = (E ▹ (λ v . result (ρ_{v}))) ▹ (λ ρ^{'} . eval (e_{2}) ρ^{'}) = E ▹ (λ v . result (ρ_{v}) ▹ (λ ρ^{'} . eval (e_{2}) ρ^{'})) = E ▹ F .

(2)

The two steps use associativity and left identity from the monad laws.

For the application, evaluating the lambda abstraction yields result c, where the programming closure

c

satisfies

apply (c, [v]) = F (v)

. The singleton argument evaluator reduces to

evalArgs ([e_{1}]) ρ = E ▹ (λ v . result ([]) ▹ (λ v s . result (v : v s))) = E ▹ (λ v . result ([v])) .

(3)

Use left identity to remove the initial result c, then associativity and left identity again:

eval ((lambda (x) e_{2}) e_{1}) ρ = (E ▹ (λ v . result ([v]))) ▹ (λ v s . apply (c, v s)) = E ▹ (λ v . result ([v]) ▹ (λ v s . apply (c, v s))) = E ▹ F .

(4)

Consequently,

eval (let val x = e_{1} in e_{2}) ρ = eval ((lambda (x) e_{2}) e_{1}) ρ for every lawful M .

(5)

The argument relies on the lambda abstraction itself being effect-free, as specified in part (a), and on using the same semantic environment for

e_{1}

on each side. No commutativity of effects is assumed. In particular, the proof applies to state monads, exceptions and continuation monads, not merely to the identity monad.

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Principles of programming languages / 3 / c / Solution 2026-10-31

 View more

Add the abstract syntax tree alternative Fix Ident Expr. Its syntactic sugar expansion and the semantic equations from part (a) give

eval (Fix x e) ρ = eval (Let (Rec x e) (Variable x)) ρ = defn (Rec x e) ρ ▹ (λ ρ^{'} . result (lookupEnv (ρ^{'}, x))) = result (ρ^{*}) ▹ (λ ρ^{'} . result (lookupEnv (ρ^{'}, x))) = result (v),

(1)

where

ρ^{*} = extend (ρ, [(x, v)])

and

v = close (e, ρ^{*})

. The final step uses left identity from the monad laws and the lookup rule for the newly bound identifier.

Thus a direct evaluator equation is:

eval (Fix x e@(Lambda xs body)) rho = result v
  where
    rho' = extend rho [(x,v)]
    v = close e rho'

Equivalently, spelling out programming closure construction,

eval (Fix x (Lambda x s b)) ρ = result (v), v = Function (λa r g s . eval (b) (extend (ρ^{*}, zip (x s, a r g s)))) .

(2)

The result is a recursive closure, not the result of calling its body. Its self-binding is visible inside that body but does not extend the caller's surrounding semantic environment.

 Read the full article