G'day all.
Quoting Benjamin Franksen
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