# Proving a monadic equivalence (Programming Languages)

Jump to navigation
Jump to search

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.