Contents
Parametric PolymorphismEdit
Section goal = short, enables reader to read code (ParseP) with ∀ and use libraries (ST) without horror. Question Talk:Haskell/The_CurryHoward_isomorphism#Polymorphic types would be solved by this section.
Link to the following paper: Luca Cardelli: On Understanding Types, Data Abstraction, and Polymorphism.
forall a
Edit
As you may know, a polymorphic function is a function that works for many different types. For instance,
length :: [a] > Int
can calculate the length of any list, be it a string String = [Char]
or a list of integers [Int]
. The type variable a
indicates that length
accepts any element type. Other examples of polymorphic functions are
fst :: (a, b) > a
snd :: (a, b) > b
map :: (a > b) > [a] > [b]
Type variables always begin in lowercase whereas concrete types like Int
or String
always start with an uppercase letter, that's how we can tell them apart.
There is a more explicit way to indicate that a
can be any type
length :: forall a. [a] > Int
In other words, "for all types a
, the function length
takes a list of elements of type a
and returns an integer". You should think of the old signature as an abbreviation for the new one with the forall
^{[1]}. That is, the compiler will internally insert any missing forall
for you. Another example: the types signature for fst
is really a shorthand for
fst :: forall a. forall b. (a,b) > a
or equivalently
fst :: forall a b. (a,b) > a
Similarly, the type of map
is really
map :: forall a b. (a > b) > [a] > [b]
The idea that something is applicable to every type or holds for everything is called universal quantification. In mathematical logic, the symbol ∀^{[2]} (an upsidedown A, read as "forall") is commonly used for that, it is called the universal quantifier.
Higher rank typesEdit
With explicit forall
, it now becomes possible to write functions that expect polymorphic arguments, like for instance
foo :: (forall a. a > a) > (Char,Bool)
foo f = (f 'c', f True)
Here, f
is a polymorphic function, it can be applied to anything. In particular, foo
can apply it to both the character 'c'
and the boolean True
.
It is not possible to write a function like foo
in Haskell98, the type checker will complain that f
may only be applied to values of either the type Char
or the type Bool
and reject the definition. The closest we could come to the type signature of foo
would be
bar :: (a > a) > (Char, Bool)
which is the same as
bar :: forall a. ((a > a) > (Char, Bool))
But this is very different from foo
. The forall
at the outermost level means that bar
promises to work with any argument f
as long as f
has the shape a > a
for some type a
unknown to bar
. Contrast this with foo
, where it's the argument f
who promises to be of shape a > a
for all types a
at the same time , and it's foo
who makes use of that promise by choosing both a = Char
and a = Bool
.
Concerning nomenclature, simple polymorphic functions like bar
are said to have a rank1 type while the type foo
is classified as rank2 type. In general, a rankn type is a function that has at least one rank(n1) argument but no arguments of even higher rank.
The theoretical basis for higher rank types is System F, also known as the secondorder lambda calculus. We will detail it in the section System F in order to better understand the meaning of forall
and its placement like in foo
and bar
.
Haskell98 is based on the HindleyMilner type system, which is a restriction of System F and does not support forall
and rank2 types or types of even higher rank. You have to enable the RankNTypes
^{[3]} language extension to make use of the full power of System F.
But of course, there is a good reason that Haskell98 does not support higher rank types: type inference for the full System F is undecidable, the programmer would have to write down all type signatures. Thus, the early versions of Haskell have adopted the HindleyMilner type system which only offers simple polymorphic function but enables complete type inference in return. Recent advances in research have reduced the burden of writing type signatures and made rankn types practical in current Haskell compilers.
runST
Edit
For the practical Haskell programmer, the ST monad is probably the first example of a rank2 type in the wild. Similar to the IO monad, it offers mutable references
newSTRef :: a > ST s (STRef s a)
readSTRef :: STRef s a > ST s a
writeSTRef :: STRef s a > a > ST s ()
and mutable arrays. The type variable s
represents the state that is being manipulated. But unlike IO, these stateful computations can be used in pure code. In particular, the function
runST :: (forall s. ST s a) > a
sets up the initial state, runs the computation, discards the state and returns the result. As you can see, it has a rank2 type. Why?
The point is that mutable references should be local to one runST
. For instance,
v = runST (newSTRef "abc")
foo = runST (readSTRef v)
is wrong because a mutable reference created in the context of one runST
is used again in a second runST
. In other words, the result type a
in (forall s. ST s a) > a
may not be a reference like STRef s String
in the case of v
. But the rank2 type guarantees exactly that! Because the argument must be polymorphic in s
, it has to return one and the same type a
for all states s
; the result a
may not depend on the state. Thus, the unwanted code snippet above contains a type error and the compiler will reject it.
You can find a more detailed explanation of the ST monad in the original paper Lazy functional state threads^{[4]}.
ImpredicativityEdit
 predicative = type variables instantiated to monotypes. impredicative = also polytypes. Example:
length [id :: forall a . a > a]
orJust (id :: forall a. a > a)
. Subtly different from higherrank.
 relation of polymorphic types by their generality, i.e. `isInstanceOf`.
 haskellcafe: RankNTypes short explanation.
System FEdit
Section goal = a little bit lambda calculus foundation to prevent brain damage from implicit type parameter passing.
 System F = Basis for all this ∀stuff.
 Explicit type applications i.e.
map Int (+1) [1,2,3]
. ∀ similar to the function arrow >.  Terms depend on types. Big Λ for type arguments, small λ for value arguments.
ExamplesEdit
Section goal = enable reader to judge whether to use data structures with ∀ in his own code.
 Church numerals, Encoding of arbitrary recursive types (positivity conditions):
&forall x. (F x > x) > x
 Continuations, Patternmatching:
maybe
,either
andfoldr
I.e. ∀ can be put to good use for implementing data types in Haskell.
Other forms of PolymorphismEdit
Section goal = contrast polymorphism in OOP and stuff. how type classes fit in.
 adhoc polymorphism = different behavior depending on type s. => Haskell type classes.
 parametric polymorphism = ignorant of the type actually used. => ∀
 subtyping
Free TheoremsEdit
Section goal = enable reader to come up with free theorems. no need to prove them, intuition is enough.
 free theorems for parametric polymorphism.
Notes
 ↑ Note that the keyword
forall
is not part of the Haskell 98 standard, but any of the language extensionsScopedTypeVariables
,Rank2Types
orRankNTypes
will enable it in the compiler. A future Haskell standard will incorporate one of these.  ↑ The
UnicodeSyntax
extension allows you to use the symbol ∀ instead of theforall
keyword in your Haskell source code.  ↑ Or enable just
Rank2Types
if you only want to use rank2 types  ↑ John Launchbury; Simon Peyton Jones (1994????). Lazy functional state threads. ACM Press". pp. 2435. http://www.dcs.gla.ac.uk/fp/papers/lazyfunctionalstatethreads.ps.Z.
See alsoEdit
 Luca Cardelli. On Understanding Types, Data Abstraction, and Polymorphism.

This page is a stub. You can help Haskell by expanding it. 