Proving a monadic equivalence (Programming Languages)

Copyright © 2024 J. M. Spivey
Jump to navigation Jump to search

The operations of a monad must obey the three laws,

  1. Associativity: (xmf) ▹ g = xm ▹ (λ xf xg),
  2. Left identity: result xf = f x,
  3. Right identity: xmresult = xm.

Together, these laws can be used to prove that the expression

let val x = E in x

has the same value as E in any environment, where E is any expression. This equivalence therefore holds in any language that contains the let val construct, whatever monad it is based on.

To prove the equivalence, let LHS be the let expression above. We use the equations,

eval (Let d e1) env = elab d env ▹ (λ env'eval e1 env'),
eval (Variable x) env = result (find env x),
elab (Val x e) env = eval e env ▹ (λ vresult (define env x v)),

to work out the meaning of LHS:

eval LHS env = (vmf) ▹ g,

where

vm = eval E env,
f v = result (define env x v),
g env' = result (find env' x).

Now we apply the associative law to obtain

eval LHS env = vm ▹ (λ vf vg).

But given v, we can write env1 = define env x v and reason as follows, using the left identity law:

f vg = result env1g = g env1 = result (find env1 x) = result v.

Therefore, applying now the right identity law,

eval LHS env = eval E env ▹ (λ vresult v) = eval E env,

as required.