proving monad laws
andrea
(return x) >>= f == f x
m >>= return == m
(m >>= f) >>= g == m >>= (\x -> f x >>= g)
If I create a new monad, should I try to see if they are actually true??
how could you prove that for any f or m?
I was trying with the simple Maybe monad with some numerical examples,
but with no luck.
*Main Monad> let t = Just 10
*Main Monad> (return t) >>= (+1)
<interactive>:1:15:
No instance for (Num (Maybe Integer))
arising from a use of `+' at <interactive>:1:15-18
Possible fix: add an instance declaration for (Num (Maybe Integer))
In the second argument of `(>>=)', namely `(+ 1)'
In the expression: (return t) >>= (+ 1)
In the definition of `it': it = (return t) >>= (+ 1)
Shouldn't be the function be of type (Integer -> Integer)? Am I missing
something (as usual)?
Gareth McCaughan
> Given the three monad laws
>
>
> (return x) >>= f == f x
> m >>= return == m
> (m >>= f) >>= g == m >>= (\x -> f x >>= g)
>
> If I create a new monad, should I try to see if they are actually true??
> how could you prove that for any f or m?
>
> I was trying with the simple Maybe monad with some numerical examples,
> but with no luck.
>
> *Main Monad> let t = Just 10
> *Main Monad> (return t) >>= (+1)
So you're trying to apply
(return x) >>= f == f x
in the case where
x == Just 10
f == (+1)
which means the RHS is
(+1) (Just 10)
or
(Just 10) + 1
which doesn't work because (Just 10) is of type Maybe Integer.
As the machine helpfully tells you:
> <interactive>:1:15:
> No instance for (Num (Maybe Integer))
> arising from a use of `+' at <interactive>:1:15-18
> Possible fix: add an instance declaration for (Num (Maybe Integer))
> In the second argument of `(>>=)', namely `(+ 1)'
> In the expression: (return t) >>= (+ 1)
> In the definition of `it': it = (return t) >>= (+ 1)
If instead you take x == 10 then you should get the right types.
(In the Maybe monad, return == Just.)
--
Gareth McCaughan
.sig under construc
Vesa Karvonen
> Given the three monad laws
> (return x) >>= f == f x
> m >>= return == m
> (m >>= f) >>= g == m >>= (\x -> f x >>= g)
> If I create a new monad, should I try to see if they are actually true??
Well, yes. To program without understanding is voodoo.
> how could you prove that for any f or m?
One way is to do a little calculation, using the definitions of the
combinators (return and >>=) and the rules of the language. You start
with the left hand side of a law and transform it step-by-step until you
reach the right hand side of the law.
As it happens, I've been recently tinkering with a monadic iterator
combinator library in Standard ML:
An iterator, or enumerator, is a higher-order function that applies a
given function to elements drawn from a sequence of some kind:
type 'a t = ('a unit) -> unit
(Note: In Haskell one possible type for the iterator monad would be
newtype Monad m => Iter m a = Iter {for :: (a -> m ()) -> m ()} .)
It turns out that iterators can be augmented to a monad with plus:
fun return x = fn e => e x
fun aM >>= a2bM = fn e => aM (fn a => a2bM a e)
val zero = fn _ => ()
fun aM <|> bM = fn e => (aM e ; bM e)
The iterator monad is related to the continuation (or cps) monad (has
similar types and implementations of return and >>=) and the list monad
(the list monad and the iterator monad satisfy the same monad and monad
plus laws). To verify that the laws really hold, I did a little
calculation. Below are proof sketches for the monad plus laws of the
iterator monad.
Left Identity (Monoid): zero <|> m = m
zero <|> m (<|>)
fn e => (zero e ; m e) (zero)
fn e => (() ; m e) (nop)
fn e => m e (eta)
m
Right Identity (Monoid): m <|> zero = m
m <|> zero (<|>)
fn e => (m e ; zero e) (zero)
fn e => (m e ; ()) (nop)
fn e => m e (eta)
m
Assoc (Monoid): (x <|> y) <|> z = x <|> (y <|> z)
(x <|> y) <|> z (<|>)
fn e => ((x <|> y) e ; z e) (<|>)
fn e => ((fn e => (x e ; y e)) e ; z e) (beta)
fn e => ((x e ; y e) ; z e) (seq)
fn e => (x e ; (y e ; z e)) (beta)
fn e => (x e ; (fn e => (y e ; z e)) e) (<|>)
fn e => (x e ; (y <|> z) e) (<|>)
x <|> (y <|> z)
Left Zero: zero >>= f = zero
zero >>= f (>>=)
fn e => zero (fn a => f a e) (zero)
fn e => (fn _ => ()) (fn a => f a e) (beta)
fn e => () (zero)
zero
Left Distribution: (x <|> y) >>= f = (x >>= f) <|> (y >>= f)
(x <|> y) >>= f (>>=)
fn e => (x <|> y) (fn a => f a e) (<|>)
fn e => (fn e => (x e ; y e)) (fn a => f a e) (beta)
fn e => (x (fn a => f a e) ; y (fn a => f a e)) (beta * 2)
fn e => ((fn e => x (fn a => f a e)) e
; (fn e => y (fn a => f a e)) e) (>>= * 2)
fn e => ((x >>= f) e ; (y >>= f) e) (<|>)
(x >>= f) <|> (y >>= f)
-Vesa Karvonen
andrea
Ok
return x == Just x
of course works, but it's not the monad law I think...
I know that the types were wrong, but I just tried to apply the law,
how can it be done then?
THanks
Gareth McCaughan
[me:]
>> If instead you take x == 10 then you should get the right types.
>> (In the Maybe monad, return == Just.)
[Andrea:]
> return x == Just x
> of course works, but it's not the monad law I think...
Why do you think that, and what do you think *is* the
monad law?
See, e.g.,
http://en.wikipedia.org/wiki/Monads_in_functional_programming
http://www.haskell.org/all_about_monads/html/maybemonad.html
http://www.randomhacks.net/articles/2007/03/12/monads-in-15-minutes
which are the top three Google results for "maybe monad"
and all mention that the Maybe monad's return is Just.
> I know that the types were wrong, but I just tried to apply the law,
> how can it be done then?
I'm afraid I don't understand the question.
andrea
> "andrea" wrote:
>
> [me:]
>
> >> If instead you take x == 10 then you should get the right types.
> >> (In the Maybe monad, return == Just.)
>
> [Andrea:]
>
> > return x == Just x
> > of course works, but it's not the monad law I think...
>
> Why do you think that, and what do you think *is* the
> monad law?
Ok this
*Transform List> (return 10 >>= Just) == Just 10
True
Looks more like the "proof" of the law, doesn't it?
Vesa Karvonen
No, your example is not a proof of the left identity law
return x >>= f = f x
for arbitrary x and f, which is what I assume you are trying to prove.
One problem with your example is that you use a specific f. Your example
would pass if one would define
return x = Just x
Nothing >>= _ = Nothing
Just x >>= _ = Just x
but the above definitions do not satisfy the left identity law, so your
example is not a sufficient condition to prove the left identity law for
the maybe monad.
The maybe monad is defined as:
return x = Just x
Nothing >>= _ = Nothing
Just x >>= f = f x
To prove the left identity law for the maybe monad, one simply needs to
observe that
return x >>= f (by definition of return)
= Just x >>= f (by definition of >>=)
= f x
which proves it.
-Vesa Karvonen
andrea
Ok thanks a lot it was easy, just apply definitions and looks if it
matches...