# Proving a monadic equivalence (Programming Languages)

Jump to: navigation, search

The operations of a monad must obey the three laws,

1. Associativity: (xm f) g = xm (λx f x g),
2. Left identity: result x f = f x,
3. 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 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 (λ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 env1 = define env x v and reason as follows, using the left identity law:

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

Therefore, applying now the right identity law,

eval LHS env = eval E env (λv result v) = eval E env,

as required.