[Haskell-cafe] A free monad theorem?
ajb at spamcop.net
ajb at spamcop.net
Mon Sep 4 00:14:13 EDT 2006
G'day all.
Quoting Benjamin Franksen <benjamin.franksen at bessy.de>:
> As we all know, the monadic bind operation has type:
>
> bind :: Monad m => m a -> (a -> m b) -> m b
>
> My intuition says that in order to apply the second argument to some
> non-trivial (i.e. non-bottom) value of type a, the bind operator needs to
> be able to somehow 'extract' a value (of type a) from the first argument
> (of type m a). I would like to argue that this is because bind is
> polymorphic in a, which makes it impossible to construct values of type
> a 'out of thin air' (besides bottom).
...which you can indeed do, and it is indeed a free theorem.
Let's forget for a moment that we know any monad laws, and only know
the laws for Functor:
fmap (f . g) = fmap f . fmap g
fmap id = id
Assuming M is a Functor, then bind, by virtue of its type alone, has
a free theorem:
forall f :: A1 -> A2
forall g :: B1 -> B2
forall m :: M A1
forall k1 :: A1 -> M B1
forall k2 :: A2 -> M B2
(
fmap g . k1 = k2 . f
=>
fmap g (m >>= k1) = (fmap f m) >>= k2
)
Setting g = id and doing a bit of rearranging and renaming gives:
forall f :: A1 -> A2
forall m :: M A1
forall k :: A1 -> M B
bind (fmap f m) k = bind m (k . f)
This gives the law for shifting f across a bind operation. To see
how "values" can be shifted, we can simply set f = const x:
forall m :: M A
forall k :: A -> M B
forall x :: A
bind (fmap (const x) m) k = bind m (\_ -> k x)
If x is a specific non-bottom value, this shows exactly how x can be
shifted from the left hand side of a bind to the right hand side. And,
as you can see, the only place where k can get the value x is from the
left-hand side.
As someone else on this thread pointed out, in category theory, monads
are usually understood in terms of these operations:
return :: a -> M a
join :: M (M a) -> M a
The bind operation can then be defined as:
bind m k = join (fmap k m)
Like the laws for bind, the laws for return and join are not
actually needed to prove the above law. You only need to assume
that M is a Functor:
bind (fmap (const x) m) k
= (defn. of bind)
join . fmap k . fmap (const x) $ m
= (M is a functor)
join . fmap (k . const x) $ m
= (defn. of bind)
bind m (k . const x)
Cheers,
Andrew Bromage
More information about the Haskell-Cafe
mailing list