Haskell/Polymorphism

From Wikibooks, the open-content textbooks collection

[edit] Parametric Polymorphism

Section goal = short, enables reader to read code (ParseP) with ∀ and use libraries (ST) without horror. Question Talk:Haskell/The_Curry-Howard_isomorphism#Polymorphic types would be solved by this section.

Link to the following paper: Luca Cardelli: On Understanding Types, Data Abstraction, and Polymorphism.

[edit] forall a

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 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 upside-down A, read as "forall") is commonly used for that, it is called the universal quantifier.

[edit] Higher rank types

With an 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, the argument f is a polymorphic function that can be applied to anything; in particular, foo may choose to apply it to characters and booleans. Do not confuse this type with

 bar :: forall a. (a -> a) -> (Char, Bool)

where the argument may only be applied to values of a certain type a which bar has no choice over.

Our example foo is said to have a rank-2 type. There are other ranks as well. Counting begins with ordinary polymorphic functions like

 id  :: forall a. a -> a
 map :: forall a. [a] -> [a]

which are said to have rank-1 types. Functions with rank-1 types as arguments have rank-2 types. Examples include

 f2  :: (forall a. a -> a -> a) -> Int -> Int
 g2  :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int

A function like

 f3  :: ((forall a. a -> a -> a) -> Int) -> Bool -> Bool

with a rank-2 type on the left of the function arrow is said to have a rank-3 type and so on.

What rank does

 const :: forall a. a -> (forall b. b -> a)

have? It's the same as

 const :: forall a. forall b. a -> b -> a

and therefor a rank-1 type. In other words, a forall can be moved to the front when it's on the right of a function arrow, i.e. in the result position. Only quantifiers on the left of a function arrow, that is in the argument position, increase the rank and cannot be moved to the front.

Since Haskell98 does not support forall and higher rank types, you have to enable the RankNTypes^[3] language extension to use functions of arbitrary rank. But there is a good reason that the Haskell98 standard does not support them: type inference for rank-n types is undecidable, the programmer would have to write down all type signatures himself. Thus, the early versions of Haskell have adopted the Hindley-Milner type system which restricts every functions to a rank-1 type but gives full type inference in return. Recent advances in research have reduced the burden of writing type signatures and made rank-n types practical in current Haskell compilers.

[edit] runST

For the practical Haskell programmer, the ST monad is probably the first example of a rank-2 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 rank-2 type. Why?

The point is that mutable references should be local to one runST. For instance,

 v   = runST (newSTRef "abc")
 foo = runST (readVar 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 rank-2 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].

[edit] Impredicativity

• predicative = type variables instantiated to monotypes. impredicative = also polytypes. Example: length [id :: forall a . a -> a] or Just (id :: forall a. a -> a). Subtly different from higher-rank.

• relation of polymorphic types by their generality, i.e. `isInstanceOf`.
• haskell-cafe: RankNTypes short explanation.

[edit] System F

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.

[edit] Examples

Section goal = enable reader to judge whether to use data structures with ∀ in his own code.

• Curch numerals, Encoding of arbitrary recursive types (positivity conditions): &forall x. (F x -> x) -> x
• Continuations, Pattern-matching: maybe, either and foldr

I.e. ∀ can be put to good use for implementing data types in Haskell.

[edit] Other forms of Polymorphism

Section goal = contrast polymorphism in OOP and stuff. how type classes fit in.

• ad-hoc polymorphism = different behavior depending on type s. => Haskell type classes.
• parametric polymorphism = ignorant of the type actually used. => ∀
• subtyping

[edit] Free Theorems

Secion goal = enable reader to come up with free theorems. no need to prove them, intuition is enough.

• free theorems for parametric polymorphism.

[edit] Footnotes

1. ↑ Note that the keyword forall is not part of the Haskell 98 standard, but any of the language extensions ScopedTypeVariables, Rank2Types or RankNTypes will enable it in the compiler. A future Haskell standard will incorporate one of these.
2. ↑ The UnicodeSyntax extension allows you to use the symbol ∀ instead of the forall keyword in your Haskell source code.
3. ↑ Or enable just Rank2Types if you only want to use rank-2 types
4. ↑ John Launchbury (1994-??-??). "Lazy functional state threads". 24-35 . ACM Press".

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