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:
runST
, foo
and bar
above).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.
Let's start with a code example:
foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
postProcess val
where
val :: b
val = maybe onNothin onJust mval
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 the b
in val :: b
the same one as the b
in foob :: 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 of forall
, and not to the ScopedTypeVariables
use.
Rank-N-Types:
Let's start with that mayb :: b -> (a -> b) -> Maybe a -> b
is equivalent to mayb :: forall a b. b -> (a -> b) -> Maybe a -> b
, except for when ScopedTypeVariables
is enabled.
This means that it works for every a
and b
.
Let's say you want to do something like this.
ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])
What must be the type of this liftTup
? It's liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
. To see why, let's try to code it:
ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
No instance for (Num [Char])
...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)
"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"
-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)
ghci> :l test.hs
Couldnt match expected type 'x' against inferred type 'b'
...
Hmm. so here GHC doesn't let us apply liftFunc
on v
because v :: b
and liftFunc
wants an x
. We really want our function to get a function that accepts any possible x
!
{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)
So it's not liftTup
that works for all x
, it's the function that it gets that does.
Existential Quantification:
Let's use an example:
-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x
ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2
How is that different from Rank-N-Types?
ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
Couldnt match expected type 'a' against inferred type '[Char]'
...
With Rank-N-Types, forall a
meant that your expression must fit all possible a
s. For example:
ghci> length ([] :: forall a. [a])
0
An empty list does work as a list of any type.
So with Existential-Quantification, forall
s in data
definitions mean that, the value contained can be of any suitable type, not that it must be of all suitable types.