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)?

Intercalation

Not sure why all the answers are so wordy. In one sentence: you’re right; it doesn’t change anything and is just there to be explicit. – Infix

The forall a b. <..> in the type of >>= is bound to a specific function - the function m a -> (a -> m b) -> m b. You can also have a forall without a function, e.g. [] :: forall a . [a], empty :: forall f a . Alternative f => f a. – Rask

@Ryan When I get the answer: "Because everything is implicitly qualified." my follow-up question is often "Why?". – Corot

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.

Surplusage

Thanks Malcolm, this is a great answer. – Intercalation

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.

Corot

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.

Engracia

Answer 4

The forall in the monad definition is only to make the universal quantification more explicit. If you have a type variable without further restrictions it is universal by default, i.e. can be anything.

So lets look at the difference between the two uses of forall and how haskell might see them:

Implicit:

foo ::  (x -> f x) -> a -> b -> (f a, f b)
-- same as
foo :: forall f x a b . (x -> f x) -> a -> b -> (f a, f b)
-- our function is applied to a, so x is equal to a
foo :: forall f x a b . (x ~ a) => (x -> f x) -> a -> b -> (f a, f b)
-- our function is also applied to b, so x is equal to b
foo :: forall f x a b . (x ~ a, x ~ b) => (x -> f x) -> a -> b -> (f a, f b)

Uh oh, (x ~ a, x~ b) would require (a ~ b). That would be inferred without annotation but since we explicitly used different type variables everything blows up. To solve this we need f to stay polymorphic within our function.

Standard haskell can't express this so we are going to need rank2types or rankntypes. With that we can write:

foo ::  (forall x . x -> f x) -> a -> b -> (f a, f b)

Note that is the forall is part of the function type. This way it stays polymorphic in our function and we can apply it to different types without everything blowing up!

Note that we also could just do:

foo :: Monad m => a -> b -> (m a, m b)
foo a b = (return a, return b)

Gerius

Actually, you don't need Monad, pure from Applicative is good enough. And actually actually Pointed is even weaker. – Corot

Good point! Is applicative a superclass of monad in the language standard yet? – Gerius

Yes, I believe since GHC 7.8. If you want to look it up it's called the AMP or Applicative-Monad proposal. – Corot