proving the monad laws

[oleg@pobox.com]

Steffen Mazanek posed a problem: given the monad:

> data Error a = Error String | Ok a
> data TI a = TI (Subst -> Int -> Error (Subst, Int, a))
> instance Monad TI where
>  return x   = TI (\s n -> Ok (s,n,x))
>  TI f >>= g = TI (\s n -> case f s n of
>                            Ok (s',m,x) -> let TI gx = g x in
>                                           gx s' m
>                            Error s->Error s)
>  fail s = TI (\_ _->Error s)

prove the associativity of bind:

> m@(TI mf) >>= (\a->f a >>= h) =
>  = TI (\s n -> case mf s n of
>       Ok (s',m,x) -> let TI gx = (\a->f a >>= h) x in
>                            gx s' m
>       Error s->Error s)  =  ...
>  = ((TI mf) >>= f) >>= h
> I was wondering, if it is possible to simplify: "let TI gx = f x >>=h in 
> ...".
> But the "a" may occur in "h"?

No, it may not. First of all, the third monadic law  specifically
disclaims such an occurrence. Indeed, if 'a' had occurred free in 'h', 
then ((TI mf) >>= f) >>= h would make no sense. 

Although (>>=) notation is better for practical programming, I
believe Filinski's notation is superior for manipulation. Filinski
defines a postfix operator "raised star", which is denoted 'st' below:

st:: (Monad m) => (a -> m b) -> m a -> m b
st f m = m >>= f

Indeed, st = flip (>>=)

In Filinski's notation, the third monadic law has an especially
appealing form:
	st ((st f) . g) = (st f) . (st g)

Let us also define 
	arun (TI f) s n = f s n

We can then write for our monad:

st f = \m -> TI $ \s n -> case arun m s n of
			     Ok (s',m',x') -> arun (f x') s' m'
			     Error s' -> Error s'

Let _m, _s and _n denote "fresh" values of the right type (so we can later
appeal to the universal generalization rule (closely related to eta-reduction)

Phase 1:

arun ((st ((st f) . g)) _m) _s _n
=>
case arun _m _s _n of
  Ok (s',m',x') -> arun ((st f) $ g x') s' m'  -- x' is not free in f, g
  Error s' -> Error s'
=>
case arun _m _s _n of
  Ok (s',m',x') -> case arun (g x') s' m' of
		      Ok (s'',m'',x'') -> arun (f x'') s'' m''
		      Error s'' -> Error s''
  Error s' -> Error s'


Phase 2:

arun (((st f) . (st g)) _m) _s _n
=>
arun (((st f) $ (st g) _m) _s _n
=>
case arun ((st g) _m) _s _n of
  Ok (s'',m'',x'') -> arun (f x'') s'' m''  -- x'' is not free in f, g
  Error s'' -> Error s''
=>
case (case arun _m _s _n of
      Ok (s',m',x') -> arun (g x') s' m'    -- x' is not free in f, g
      Error s' -> Error s') of
  Ok (s'',m'',x'') -> arun (f x'') s'' m''  -- x'' is not free in f, g
  Error s'' -> Error s''
=> {see note below}
case arun _m _s _n of
  Ok (s',m',x') -> case arun (g x') s' m' of
                       Ok (s'',m'',x'') -> arun (f x'') s'' m''
		       Error s'' -> Error s''
  Error s' -> Error s'

Now, the results of Phase 1 and Phase 2 are identical.  Given that _m,
_s and _n were unique, fresh variables, by appealing to the universal
generalization rule and the Church-Rosser property of our reductions,
we conclude that

	st ((st f) . g) = (st f) . (st g)

The critical step is the associativity of case:

  case (case x of C1 -> O1; C2 -> O2) of C1' -> O1'; C2' -> O2'
==>
  case x of 
     C1 -> case O1 of C1' -> O1'; C2' -> O2'
     C2 -> case O2 of C1' -> O1'; C2' -> O2'
	
provided that variables bound in C1 and C2 do not occur in C1', O1', C2', O2'