Proving a monadic equivalence (Programming Languages)
From Spivey's Corner
The operations of a monad must obey the three laws,
- Associativity: (xm ▷ f) ▷ g = xm ▷ (λx → f x ▷ g),
- Left identity: result x ▷ f = f x,
- Right identity: xm ▷ result = 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 e_{1}) env = elab d env ▷ (λenv' → eval e_{1} env'),
- eval (Variable x) env = result (find env x),
- elab (Val x e) env = eval e env ▷ (λv → result (define env x v)),
to work out the meaning of LHS
:
- eval LHS env = (vm ▷ f) ▷ 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 ▷ (λv → f v ▷ g).
But given v, we can write env_{1} = define env x v and reason as follows, using the left identity law:
- f v ▷ g = result env_{1} ▷ g = g env_{1} = result (find env_{1} x) = result v.
Therefore, applying now the right identity law,
- eval LHS env = eval E env ▷ (λv → result v) = eval E env,
as required.