Understanding forall in Monad '>>=' function?

Question

Following this answer, I've implemented a generic lift function in my program:

liftTupe :: (x -> c x) -> (a, b) -> (c a, c b) --This will error
liftTuple :: (forall x. x -> c x) -> (a, b) -> (c a, c b)

I understand, that in this context, forall is enabling x to be of any type ([], Maybe etc..).

I'm now looking into the definition of >>= in Monads:

class Applicative m => Monad m where
   (>>=) :: forall a b. m a -> (a -> m b) -> m b

I'm can't understand the role of this forall in the function definition? As, unlike liftTuple, it's not bound to a specific function (x -> c x)?

Answer 1

Basically, when you don't use forall, all the types are global in the function definition, which means they are all deduced when the function is called. With forall you can forego that for the function taking x until it is called itself.

So in the first one you have a function which takes x and gives c x, then you have a tuple with a and b and you expect a tuple with c a and c b. Since you already said that the first function accepts x, you can make x become the same as a, but it won't be b then because x is defined once for the whole declaration. So you can't make the function accept both a and b.

However, in the second case the x scope is limited to the function taking x. We're basically saying that there is a function which takes something and makes c with that something, and it can be any type. That enables us to first feed a to it and then b, and it will work. x doesn't have to be something singular now outside.

What you are seeing in the Monad definition is the "ExplicitForAll" language extension. There is a description on Haskell Prime for this extension

ExplicitForAll enables the use of the keyword 'forall' to explicitly state that a type is polymorphic in its free type variables. It does not allow any types to be written that cannot already be written; it just allows the programmer to explicitly state the (currently implicit) quantification.

This language extension is purely visual, allows you to write out the variables explicitly which you previously couldn't. You can simply omit forall a b. from the Monad declaration, and the program will functionally stay exactly the same.

Say, with this extension you could rewrite the liftTupe as forall a b x. (x -> c x) -> (a, b) -> (c a, c b). The definition is the same and it functions the same, but readers will now clearly see that the type variables are all defined on the topmost level.

Answer 2

Every function you write is implicitly universally quantified over its type variables:

id :: a -> a           -- this is actually universally quantified over a
id :: forall a. a -> a
id x = x

You can actually turn this behaviour on with the ExplicitForall language pragma.

This property is very useful, since it constrains you from writing code that only works with some types. Think about what the id function can do: it can either return its argument or loop forever. These are the only two things it can do and you can figure that out based on its type signature.

Enforcing all instances of polymorphic function to behave the same way, irrespective of the type argument is called parametricity and is explained in this blog post by Bartosz Milewski. The TL;DR is: Using parametricity, we can guarantee that some reorderings in out program's structure do not affect it's behaviour. For a mathematically more rigorous treatment of this, see Theorems for free! by Philip Wadler.

Answer 3

All type variables in Haskell's type system are quantified by a forall. However, GHC can infer the quantification in many cases so you don't need to write them in source code.

For example the type of liftTuple with the forall explicit is

liftTuple :: forall c a b. (forall x. x -> c x) -> (a, b) -> (c a, c b)

And for >>= the case is the same.