“forall” is the type-level “lambda”

In Haskell we write:

mkList :: a -> [a]

But PureScript requires a seemingly extraneous bit in there:

mkList :: forall a. a -> [a]

What’s up with that forall? Do we need it? And why?

Photo by Fabien Barral

Generic parameters

A friend of mine shared his intuition about generic parameters: “I always saw them as type placeholders and that every a had to be same, e.g. once a is String, all occurrences of a are String".

A reasonable assumption, but not quite true :-)

Consider this:

f :: Read a => String -> [a]
f s = g ("[" ++ s ++ "]")
   where
      g :: String -> a
      g a = read a

This program wouldn’t compile. Can you guess why?

If you stare at it long enough, you can notice that there is no good way to substitute a: if you say that a ~ Int, then f :: String -> [Int], but g :: String -> Int, so the return types don’t match.

A very reasonable analysis. And yet, the following does work:

f :: Read a => String -> [a]
f s = g ("[" ++ s ++ "]")
   where
      g :: Read a => String -> a
      g a = read a

I just added a Read a constraint to the signature of g, and now it works! Why? There is clearly still no good way to substitute a, but somehow that doesn’t matter.

Scope

The answer is that the a in f and the a in g are not the same a! They’re two different, independent type variables, that just happen to be namesakes. When the call g ("[" ++ s ++ "]") is made, the compiler makes a substitution g.a ~ [f.a], and it all works out.

That’s the default Haskell rule for type variable scope: type variables are scoped just to the signature in which they appear, and no further. Oh, except in type classes, where they’re scoped to the whole body of the type class. A bit confusing, isn’t it?

Explicit scope

It is possible to explicitly control the way that type variables are scoped. In Haskell, we need ScopedTypeVariables and ExplicitForall to do that. With these extensions enabled (note that the former will automatically turn on the latter), one can use forall in function type signatures:

f :: forall a. Read a => String -> [a]
f s = g ("[" ++ s ++ "]")
   where
      g :: String -> [a]
      g a = read a

Now the type variable a is scoped to the whole body of f — including g and its signature. That’s why I don’t need an extra Read a constraint on g — that constraint already comes from the signature of f. And of course, now that it’s the same a in both signatures, I had to change the return type of g from a to [a] .

Analogy to values

In Haskell the forall is still optional, even when it’s allowed, but in PureScript it’s required everywhere. Why would that be? Isn’t it nicer to have type variables just sort of “appear” and not bother with that extra forall?

Personally, I find explicit forall useful, because it makes the code more rigid and obvious. Consider the following lambda-expression:

f = \x -> x + 1

Wouldn’t it be nicer not to write the lambda part? What if we could write this:

f = x + 1

and have the compiler sort of “assume” that x is a free variable in that expression?

Sounds crazy? But that’s exactly what we do with types!

At value level:
   We write:                \x -> Just x
   We wish we could write:  Just x
At type level:
   We write:                forall a. Maybe a
   We wish we could write:  Maybe a

forall plays the role of lambda at the type level.