# Proving a monadic equivalence (Programming Languages)

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.