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'