Re: proving the monad laws
Hello! > Would it be possible to write a piece of Haskell code which checks > the monadic laws automatically by simulating evaluation in this way? To some extent, yes. The proof in the previous message was based on normalization, with respect to associative laws and some betas. So we can take (st f) . (st g) and do: - inlining of the 'st' operation - de-sugaring into core Haskell - more inlining and beta [perhaps to a certain depth] - rearranging expression based on associative laws, e.g., converting f . (g . h) into (f . g) . h converting case (case x of P -> A) of P' -> A' into case x of P -> case A of P' -> A' Then do the same for (st ((st f) . g)) and compare the results. If the results are identical, great. Otherwise, the user has to look at the results and decide if they are the same based on his intuition. GHC already does inlining, de-sugaring, and some betas. I think there is a flag that makes GHC dump the result of these operations for normalization with respect associative laws. BTW, GHC accepts user-defined rules: so we can express associativity rules for known operations and direct GHC to normalize terms with respect to these laws. I don't know how to express side conditions though (e.g., the normalization of 'case' above is valid only if the variables bound by pattern P do not occur in P', A'). It would be great if there was a RULES-pragma operation to alpha-rename bound variables in a term. In that case, we can safely normalize more expressions. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: proving the monad laws
Hello, thank you for the idea of using variables directly to see what happens. This is really a simplification for the proof. At first I thought that there should be a simpler solution and I tried to modify your approach, so that it applies to >>= as well, but now I am convinced :-) I have downloaded the paper of Filinski "Representing Monads" to take a look at the definition directly. It seems to be interesting for me, but deterringly difficult as well :-( Would it be possible to write a piece of Haskell code which checks the monadic laws automatically by simulating evaluation in this way? Maybe a little theoretical section in the monad tutorial which deals with this stuff would be a help as well. Iavor, I am really happy, that this monad is working :-) Never touch a running system or try to make it more difficult as it is! These monad transformers are still a red rag to me. Nevertheless thank you. Ciao, Steffen ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: proving the monad laws
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'
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: proving the monad laws
hi, just a comment that the you can get more modular (and hence simpler) proofs by using monad transformers. than you can break down your proof in a number of steps: 1. prove that the identity monad is a monad 2. prove that the exception transformer: ErrorT x m a = m (Either x a) gives a monad,if 'm' is a monad. 3. prove that the state transformer: StateT s m a = s -> m (a,s) gives a monad,provided that 'm' is a monad then you are done, as TI = StateT Subst (StateT Int (ErrorT String Id)). this involves more proofs, but they are "simpler" and can be reused for other monads as well. hope this helps iavor Steffen Mazanek wrote: Hello, consider the following monad (which is a slight adaptation of the one used in "Typing Haskell in Haskell") as given: 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) Now I would like to verify the monad laws. It is really easy to show that return is both a left- and a right-unit. But I got stuck with associativity: 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 Is there someone outside who is willing to tell what fills the gap? A hint may be sufficient already. Or is there a tool, which finds such derivations? I have read the tutorial "All about Monads", but there only is mentioned, that there is an obligation for the programmer to prove these laws. It would be helpful as well, to provide an example! I was wondering, if it is possible to simplify: "let TI gx = f x >>=h in ...". But the "a" may occur in "h"? Thank you. Steffen ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell -- == | Iavor S. Diatchki, Ph.D. student | | Department of Computer Science and Engineering | | School of OGI at OHSU | | http://www.cse.ogi.edu/~diatchki | == ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
proving the monad laws
Hello, consider the following monad (which is a slight adaptation of the one used in "Typing Haskell in Haskell") as given: 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) Now I would like to verify the monad laws. It is really easy to show that return is both a left- and a right-unit. But I got stuck with associativity: 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 Is there someone outside who is willing to tell what fills the gap? A hint may be sufficient already. Or is there a tool, which finds such derivations? I have read the tutorial "All about Monads", but there only is mentioned, that there is an obligation for the programmer to prove these laws. It would be helpful as well, to provide an example! I was wondering, if it is possible to simplify: "let TI gx = f x >>=h in ...". But the "a" may occur in "h"? Thank you. Steffen ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
