[Haskell-cafe] A free monad theorem?

[ajb at spamcop.net]

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