I'm beginning to understand how the forall
keyword is used in so-called "existential types" like this:
data ShowBox = forall s. Show s => SB s
This is only a subset, however, of how forall
is used and I simply cannot wrap my mind around its use in things like this:
runST :: forall a. (forall s. ST s a) -> a
Or explaining why these are different:
foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))
Or the whole RankNTypes
stuff…
I tend to prefer clear, jargon-free English rather than the kinds of language which are normal in academic environments. Most of the explanations I attempt to read on this (the ones I can find through search engines) have these problems:
- They're incomplete. They explain one part of the use of this keyword (like "existential types") which makes me feel happy until I read code that uses it in a completely different way (like
runST
,foo
andbar
above). - They're densely packed with assumptions that I've read the latest in whatever branch of discrete math, category theory or abstract algebra is popular this week. (If I never read the words "consult the paper whatever for details of implementation" again, it will be too soon.)
- They're written in ways that frequently turn even simple concepts into tortuously twisted and fractured grammar and semantics.
So…
On to the actual question. Can anybody completely explain the forall
keyword in clear, plain English (or, if it exists somewhere, point to such a clear explanation which I've missed) that doesn't assume I'm a mathematician steeped in the jargon?
Edited to add:
There were two stand-out answers from the higher-quality ones below, but unfortunately I can only choose one as best. Norman's answer was detailed and useful, explaining things in a way that showed some of the theoretical underpinnings of forall
and at the same time showing me some of the practical implications of it. yairchu's answer covered an area nobody else mentioned (scoped type variables) and illustrated all of the concepts with code and a GHCi session. Were it possible to select both as best, I would. Unfortunately I can't and, after looking over both answers closely, I've decided that yairchu's slightly edges out Norman's because of the illustrative code and attached explanation. This is a bit unfair, however, because really I needed both answers to understand this to the point that forall
doesn't leave me with a faint sense of dread when I see it in a type signature.
Best Answer
Let's start with a code example:
This code doesn't compile (syntax error) in plain Haskell 98. It requires an extension to support the
forall
keyword.Basically, there are 3 different common uses for the
forall
keyword (or at least so it seems), and each has its own Haskell extension:ScopedTypeVariables
,RankNTypes
/Rank2Types
,ExistentialQuantification
.The code above doesn't get a syntax error with either of those enabled, but only type-checks with
ScopedTypeVariables
enabled.Scoped Type Variables:
Scoped type variables helps one specify types for code inside
where
clauses. It makes theb
inval :: b
the same one as theb
infoob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
.A confusing point: you may hear that when you omit the
forall
from a type it is actually still implicitly there. (from Norman's answer: "normally these languages omit the forall from polymorphic types"). This claim is correct, but it refers to the other uses offorall
, and not to theScopedTypeVariables
use.Rank-N-Types:
Let's start with that
mayb :: b -> (a -> b) -> Maybe a -> b
is equivalent tomayb :: forall a b. b -> (a -> b) -> Maybe a -> b
, except for whenScopedTypeVariables
is enabled.This means that it works for every
a
andb
.Let's say you want to do something like this.
What must be the type of this
liftTup
? It'sliftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
. To see why, let's try to code it:"Hmm.. why does GHC infer that the tuple must contain two of the same type? Let's tell it they don't have to be"
Hmm. so here GHC doesn't let us apply
liftFunc
onv
becausev :: b
andliftFunc
wants anx
. We really want our function to get a function that accepts any possiblex
!So it's not
liftTup
that works for allx
, it's the function that it gets that does.Existential Quantification:
Let's use an example:
How is that different from Rank-N-Types?
With Rank-N-Types,
forall a
meant that your expression must fit all possiblea
s. For example:An empty list does work as a list of any type.
So with Existential-Quantification,
forall
s indata
definitions mean that, the value contained can be of any suitable type, not that it must be of all suitable types.