Search code examples
haskellmonadsforall

Understanding forall in Monad '>>=' function?


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


Solution

  • 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.