Chapter 7
Parametricity
Write down the definition of a polymorphic function on a piece of
paper. Tell me its type, but be careful not to let me see the function’s
definition. I will tell you a theorem that the function satisfies. –
Philip Wadler, “Theorems for free!”
Polymorphism allows a single piece of code to be instantiated with multiple
types. Polymorphism is parametric when all of the instances behave uniformly.
This is in contrast to ad-hoc polymorphism, where values can behave differently
depending on which type they are being instantiated with.
Parametricity can be thought of as the dual to abstraction. Where abstrac-
tion hides details about an implementation from the outside world, parametric-
ity hides details about the outside world from an implementation.
7.1 Parametricity in OCaml
7.1.1 Universal types in OCaml
Universal types are the most common form of parametricity in OCaml. As dis-
cussed in Chapter 3, ML polymorphism provides simple universal types without
any type annotations. For example, the polymorphic identity function, which
has type ∀𝛼.𝛼 → 𝛼:
l e t f x = x
However, this only provides rank-1 or prenex polymorphism, which means
that all universal quantifiers (∀) must appear at the out-most position (i.e. at
the very beginning of the type expression). It does not support higher-rank
universal types such as (∀𝛼.List𝛼 → Int) → Int.
Type inference for higher-rank universal types is undecidable in general. As
an illustration, consider the following OCaml function:
fun f x y -> f x + f y
This expression could have a number of System F𝜔 types, including:
85
86 CHAPTER 7. PARAMETRICITY
∀𝛼 : : * . (𝛼 → Int ) → 𝛼 → 𝛼 → Int
∀𝛼 : : * . ∀𝛽 : : * . (∀𝛾 : : * . 𝛾 → Int ) → 𝛼 → 𝛽 → Int
and none of these types is more general than the others, so we require some
annotations in order to type-check programs involving higher-rank universals.
The required annotations include explicit type abstraction and type application
statements, as well as explicitly specifying the type of the universal created by
a type abstraction.
Rather than directly using type application and type abstraction with type
annotations, universal types in OCaml are provided through record types (sim-
ilar support is also available through object types). Constructing the record
type acts as a type abstraction statement, and destructing the record using a
pattern or projection acts as a type application statement. The declaration of
a record type includes specifying the types of its fields, which provide us with
the required type annotations for type abstraction statements.
The following definition defines a type corresponding to ∀𝛼.List𝛼 → 𝐼𝑛𝑡:
type t = { f : ’ a . ’ a l i s t -> int }
Building a value of type t corresponds to a type abstraction operation:
l e t len = { f = List . length}
Destructing a value of type t using a pattern or projection corresponds to
type application:
l e t g r = r . f [ 1 ; 2 ; 3 ] + r . f [ 1 . 0 ; 2 . 0 ; 3 . 0 ]
7.1.2 Functors
The most powerful form of parametricity in OCaml is provided by functors.
Functors are functions that operate on modules. Since modules can contain any
OCaml definition, functors can be parametric on any OCaml definition.
As an example, we will extend our IntSet module to a Set module that works
uniformly on any module that matches the appropriate signature.
For convenience, we will define a module type for the signature that we
expect of arguments to the functor:
module type Eq = s ig
type t
val equal : t -> t -> bool
end
This signature says that we expect the module to contain a type t and a
function equal for comparing two values of type t for equality.
We also create a signature of the functor’s result:
module type SetS = s ig
type t
type e l t
val empty : t
val is_empty : t -> bool
7.1. PARAMETRICITY IN OCAML 87
val mem : e l t -> t -> bool
val add : e l t -> t -> t
val remove : e l t -> t -> t
val to_l i s t : t -> e l t l i s t
end
Now we define our Set functor as follows:
module Set (E : Eq) : SetS with type e l t := E. t = struct
type t = E. t l i s t
l e t empty = [ ]
l e t is_empty = function
| [ ] -> true
| _ -> f a l s e
l e t rec mem x = function
| [ ] -> f a l s e
| y : : r e s t ->
i f (E. equal x y) then true
e l s e mem x res t
l e t add x t =
i f (mem x t ) then t
e l s e x : : t
l e t rec remove x = function
| [ ] -> [ ]
| y : : r e s t ->
i f (E. equal x y) then re s t
e l s e y : : ( remove x re s t )
l e t to_l i s t t = t
end
Note that we have specified the result of the functor to have the signature
SetS with type elt := E.t. This signature is the same as SetS but with the elt
type component removed and all occurrences of it replaced by E.t. If we had
wanted to leave the elt type in the signature, but changed from an abstract type
to an alias for E.t, we could instead have used SetS with type elt = E.t.
We can apply the functor to recreate IntSet:
module IntEq = struct
type t = int
l e t equal (x : int ) (y : int ) =
x = y
end
module IntSet = Set ( IntEq)
Since the type E.t is abstract within the body of Set, the implementation
of Set can only pass these values around and compare them using E.equals, it
cannot use values of type E.t in any other way because the it cannot see the
type’s definition. This means that the behaviour of Set cannot depend on the
88 CHAPTER 7. PARAMETRICITY
particular type used for E.t: it must behave uniformly on any Eq module that
it is applied to.
7.2 Higher-kinded polymorphism
Modules and functors allow abstraction and parametricity for both types (with
kind ∗) and type constructors (with kind ∗ → ∗). However, the existential
and universal polymorphism in the core language only supports types with kind
∗. The reason for this is that type-checking higher-kinded polymorphism, re-
quires type annotations on type application as well as type abstraction. The
module system includes such annotations, but the core language avoids all such
annotations as too verbose.
As an example, consider trying to type-check applications of a function with
type ∀𝐹 ∶∶ ∗ → ∗.∀𝛼 ∶∶ ∗.𝐹 𝛼 → (𝐹 𝛼 → 𝛼) → 𝛼 to a value with type
List(Int × Int). This involves unifying the following two types:
𝐹 𝛼 ∼ List(Int × Int)
There are many possible solutions to this unification, including:
𝐹 = List 𝛼 = Int × Int
𝐹 = Λ𝛽.List(𝛽 × 𝛽) 𝛼 = Int
𝐹 = Λ𝛽.List(Int × Int)
None of which is more general than the others.
7.2.1 Lightweight higher-kinded polymorphism
It is possible to restrict higher-kinded polymorphism so that it can be type-
checked without type annotations on type applications. By restricting the type
functions which can be used to a set of functions for which each function maps
to a different set of types. In other words, a set F of functions such that:
∀𝐹, 𝐺 ∈ F. 𝐹 ≠ 𝐺 ⇒ ∀𝑡.𝐹(𝑡) ≠ 𝐺(𝑡)
This is how Haskell provides higher-kinded polymorphism: it only supports
type constructors which create fresh types. For example, Haskell has no equiv-
alent of the OCaml type1:
type ’a t = ( ’ a * ’a) l i s t
This restricted form of higher-kinded polymorphism can also be used in
OCaml with an encoding based on defunctionalisation (Reynolds [1972]). For
example, the following type definition:
1A Haskell type synonym can be created which looks like this OCaml definition, however
it is very different because it cannot be abstracted
7.3. PARAMETRICITY IN SYSTEM FΩ 89
type l s t = List
type opt = Option
type ( ’ a , ’ f ) app =
| Lst : ’ a l i s t -> ( ’ a , l s t ) app
| Opt : ’ a option -> ( ’ a , opt ) app
Allows us to represent ’a list as (’a, lst) app and ’a option as (’a, opt) app. Then
we can use polymorphism in the second parameter of app to encode higher-
kinded polymorphism over list and option. For example:
type ’ f map = {
map: ’ a ’b . ( ’ a -> ’b) -> ( ’ a , ’ f ) app -> ( ’b , ’ f ) app ;
}
l e t lmap : l s t map = {map = fun f ( Lst l ) -> Lst ( List .map f l )}
l e t omap : opt map = {map = fun f (Opt o) -> Opt (Option .map f o)}
l e t f : ’b map -> ( int , ’b) app -> ( str ing , ’b) app =
fun m c -> m.map ( fun x -> ” Int : ” ^ ( string_of_int x) ) c
l e t l = f lmap (Lst [ 1 ; 2 ; 3 ] )
l e t o = f omap (Opt (Some 6) )
The higher library (Yallop and White [2014]), extends this idea by providing
a general app type that any type constructor can be injected into.
7.3 Parametricity in System F𝜔
7.3.1 Universal types
OCaml functors with abstract types in their arguments correspond to universal
types in System F𝜔. This is not surprising: universal types are the fundamental
concept of the polymorphic lambda calculus (System F), which is intended to
capture the essence of parametric polymorphism.
As an example we will implement our Set functor using universals in Sys-
tem F𝜔.
First, for convenience, we create a type constructor and some functions for
dealing with the products that represent the structures of both the argument
and result structures of Set:
EqImpl =
𝜆𝛾 : : * . 𝛾 → 𝛾 → Bool ;
equal = Λ𝛾 : : * . 𝜆s : EqImpl 𝛾 . s ;
SetImpl =
𝜆𝛾 : : * . 𝜆𝛼 : : * .
𝛼
× (𝛼 → Bool )
× (𝛾 → 𝛼 → Bool )
× (𝛾 → 𝛼 → 𝛼)
× (𝛾 → 𝛼 → 𝛼)
× (𝛼 → List 𝛾 ) ;
90 CHAPTER 7. PARAMETRICITY
empty = Λ𝛾 : : * . Λ𝛼 : : * . 𝜆s : SetImpl 𝛾 𝛼 .𝜋1 s ;
is_empty = Λ𝛾 : : * . Λ𝛼 : : * . 𝜆s : SetImpl 𝛾 𝛼 .𝜋2 s ;
mem = Λ𝛾 : : * . Λ𝛼 : : * . 𝜆s : SetImpl 𝛾 𝛼 .𝜋3 s ;
add = Λ𝛾 : : * . Λ𝛼 : : * . 𝜆s : SetImpl 𝛾 𝛼 .𝜋4 s ;
remove = Λ𝛾 : : * . Λ𝛼 : : * . 𝜆s : SetImpl 𝛾 𝛼 .𝜋5 s ;
to_l i s t = Λ𝛾 : : * . Λ𝛼 : : * . 𝜆s : SetImpl 𝛾 𝛼 .𝜋6 s ;
Now we can create our implementation of sets, using Λ to give it a universal
type corresponding to the type of the Set functor.
set_package =
Λ𝛾 : : * . 𝜆eq : EqImpl 𝛾 .
pack List 𝛾 ,〈
n i l [𝛾 ] ,
isempty [𝛾 ] ,
𝜆n :𝛾 . f o ld [𝛾 ] [ Bool ]
(𝜆x :𝛾 .𝜆y : Bool . or y ( equal [𝛾 ] eq n x) )
fa l s e ,
cons [𝛾 ] ,
𝜆n :𝛾 . f o ld [𝛾 ] [ L i st 𝛾 ]
(𝜆x :𝛾 .𝜆 l : L i st 𝛾 .
i f ( equal [𝛾 ] eq n x) [ List 𝛾 ] l ( cons [𝛾 ] x l ) )
( n i l [𝛾 ] ) ,
𝜆 l : L i st 𝛾 . l 〉
as ∃𝛼 : : * . SetImpl 𝛾 𝛼 ;
If we look at the typing rules for universals (Section 2.3), we can see that
the type parameter of Λ is a fresh type variable. As with abstract types in the
parameters of OCaml functors, this means the body of set_package can only
pass these values around and compare them using eq, it cannot use values of
type 𝛾 in any other way because the it cannot see the type’s definition.
This means that the behaviour of set_package cannot depend on the par-
ticular type used for 𝛾: it must behave uniformly on any type that it is applied
to.
7.3.2 Relational parametricity
We can also use the relational interpretation to give a precise meaning to the
idea that universal types provide parametricity.
Given a type 𝑇 with free variables 𝛼, 𝛽1, … , 𝛽𝑛:
∀𝐵1. … ∀𝐵𝑛. ∀𝑥 ∶ (∀𝛼.𝑇 [𝛼, 𝐵1, … , 𝐵𝑛]).
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.J𝑇 K[𝜌, =𝐵1 , … , =𝐵𝑛 ](𝑥[𝛾], 𝑥[𝛿])
This formula can be read as: For a value 𝑥 with universal type, two types 𝛾
and 𝛿, and any way of viewing 𝛾 and 𝛿 as representing the same thing – captured
by a relation 𝜌 – 𝑥[𝛾] will behave the same as 𝑥[𝛿] with respect to 𝜌.
This is the essence of parametricity: a value with universal type will behave
uniformly for any types it is applied to.
7.3. PARAMETRICITY IN SYSTEM FΩ 91
The above parametricity property for universal types can be derived from
identity extension applied to universals by expanding out the relational inter-
pretationx.
7.3.3 Theorems for free
In the previous chapter we applied the abstraction property to a particular
kind of relation to show that abstraction guarantees code outside of a compo-
nent preserves invariants. Similarly, we can apply the parametricity property
to particular relations to show that parametricity guarantees code inside of a
component behaves in certain ways.
For example, applying parametricity to the type ∀𝛼.𝛼 → 𝛼, gives us the
following formula:
∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼).
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.
𝜌(𝑢, 𝑣) ⇒ 𝜌(𝑓[𝛾] 𝑢, 𝑓[𝛿] 𝑣)
By defining a relation is𝑢 to represent being equal to a value 𝑢 ∶ 𝑇 :
is𝑢(𝑥 ∶ 𝑇 , 𝑦 ∶ 𝑇 ) = (𝑥 =𝑇 𝑢) ∧ (𝑦 =𝑇 𝑢)
and using it to instantiate 𝜌, we obtain the following formula:
∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼).
∀𝛾.∀𝑢 ∶ 𝛾.
is𝑢(𝑢, 𝑢) ⇒ is𝑢(𝑓[𝛾]𝑢, 𝑓[𝛾]𝑢)
which can be reduced to:
∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼).
∀𝛾.∀𝑢 ∶ 𝛾.
𝑓[𝛾] 𝑢 =𝛾 𝑢
This shows that any value 𝑓 of type ∀𝛼.𝛼 → 𝛼 must be the identity func-
tion. Properties like this, which use parametricity to give guarantees about the
behaviour of all values of a given type, are often called free theorems after an
influential paper on the subject (Wadler [1989]).
As a second example, we can apply parametricity to the type ∀𝛼.List𝛼 →
List𝛼:
∀𝑓 ∶ (∀𝛼.List𝛼 → List𝛼).
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑢 ∶ List 𝛾. ∀𝑣 ∶ List 𝛿.JList𝛼K[𝜌](𝑢, 𝑣) ⇒ JList𝛼K[𝜌](𝑓[𝛾] 𝑢, 𝑓[𝛿] 𝑣)
(7.1)
92 CHAPTER 7. PARAMETRICITY
Applying the relational interpretation to the System F encoding of List gives
the following equation:
JList𝛼K[𝜌] =
(𝑥 ∶ List𝐴, 𝑦 ∶ List𝐵).
∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.
∀𝑛 ∶ 𝛾. ∀𝑚 ∶ 𝛿.
∀𝑐 ∶ 𝐴 → 𝛾 → 𝛾. ∀𝑑 ∶ 𝐵 → 𝛿 → 𝛿.
𝜌′(𝑛, 𝑚) ⇒
(∀𝑎 ∶ 𝐴. ∀𝑏 ∶ 𝐵. ∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿.
𝜌(𝑎, 𝑏) ⇒ 𝜌′(𝑢, 𝑣) ⇒ 𝜌′(𝑐 𝑎𝑢, 𝑑 𝑏𝑣)) ⇒
𝜌′(𝑥[𝛾]𝑛𝑐, 𝑦[𝛿]𝑚𝑑)
which can be reduced to a more manageable form by considering the cases of
𝑛𝑖𝑙 and 𝑐𝑜𝑛𝑠 separately:JList𝛼K[𝜌](𝑥 ∶ List𝐴, 𝑦 ∶ List𝐵) =
⎧{
⎨{⎩
𝜌(𝑖, 𝑗) ∧ JList𝛼K[𝜌](𝑙, 𝑘), 𝑥 = 𝑐𝑜𝑛𝑠𝐴 𝑖 𝑙 ∧ 𝑦 = 𝑐𝑜𝑛𝑠𝐵 𝑗𝑘
𝑡𝑟𝑢𝑒, 𝑥 = 𝑛𝑖𝑙𝐴 ∧ 𝑦 = 𝑛𝑖𝑙𝐵
𝑓𝑎𝑙𝑠𝑒, 𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒
(7.2)
By defining a family of relations ⟨𝑔⟩ to represent functions 𝑔 ∶ 𝐴 → 𝐵:
⟨𝑔⟩(𝑥 ∶ 𝐴, 𝑦 ∶ 𝐵) = (𝑔 𝑥 =𝐵 𝑦)
and substituting it for 𝜌 in 7.2, we obtain the following equation:
JList𝛼K[⟨𝑔⟩](𝑥 ∶ List𝐴, 𝑦 ∶ List𝐵) =
⎧{
⎨{⎩
𝑔 𝑖 =𝐵 𝑗 ∧ JList𝛼K[⟨𝑔⟩](𝑙, 𝑘), 𝑥 = 𝑐𝑜𝑛𝑠𝐴 𝑖 𝑙 ∧ 𝑦 = 𝑐𝑜𝑛𝑠𝐵 𝑗𝑘
𝑡𝑟𝑢𝑒, 𝑥 = 𝑛𝑖𝑙𝐴 ∧ 𝑦 = 𝑛𝑖𝑙𝐵
𝑓𝑎𝑙𝑠𝑒, 𝑜𝑡ℎ𝑒𝑟𝑤𝑖𝑠𝑒
This recursive equation may look quite familiar. It bears a striking resemblance
to the definition of the standard map function for lists. In fact, we can use map
to rewrite it as: JList𝛼K[⟨𝑔⟩](𝑥 ∶ List𝐴, 𝑦 ∶ List𝐵) =
map[𝐴][𝐵] 𝑔 𝑥 =𝐵 𝑦
(7.3)
Substituting 7.3 into 7.1 we get a free theorem for ∀𝛼.List𝛼 → List𝛼:
∀𝑓 ∶ (∀𝛼.List𝛼 → List𝛼).
∀𝛾. ∀𝛿. ∀𝑔 ∶ 𝛾 → 𝛿
∀𝑢 ∶ List 𝛾. ∀𝑣 ∶ List 𝛿.
map[𝛾][𝛿] 𝑔 (𝑓[𝛾] 𝑢) = 𝑓[𝛿] (map[𝛾][𝛿] 𝑔 𝑢)
An interesting corollary of this theorem is that any function 𝑓 of type
∀𝛼.List𝛼 → List𝛼 is a “rearrangement” function: the output of 𝑓 is a list
whose elements all come from the input to 𝑓 .
7.4. PRACTICAL LIMITATIONS 93
7.4 Practical limitations
The previous chapter and this one have described how abstraction and para-
metricity can give guarantees about program behaviour. However, these guaran-
tees rely on some assumptions that do not necessarily hold in real programming
languages.
7.4.1 Side-effects
In a pure language such as System F𝜔, a function accepts an input value and
produces an output value. The relation between inputs and outputs completely
defines the behaviour of a function. However, programming languages are not
generally pure, they allow functions to perform side-effects. Such side-effects
include:
• Printing to the console
• Raising exceptions
• Failing to terminate
Side-effects affect the guarantees that are provided by abstraction and para-
metricity. For example, we showed that parametricity ensures that all functions
of type ∀𝛼.𝛼 → 𝛼 are the identity function. However, the following three OCaml
functions have that type and are not the identity function:
l e t f (x : ’ a ) : ’ a =
Print f . p r in t f ”Launch mi s s i l e s \n” ;
x
l e t f (x : ’ a ) : ’ a = ra i s e Exit
l e t rec f (x : ’ a ) : ’ a = f x
The issue here is that the function type in OCaml is a different type from
the function type in System F – since it supports side-effects. This means that
the relational interpretation for OCaml’s function type is different from the
relational interpretation that we gave for System F. The relational interpretation
for OCaml’s function type should ensure not only that related inputs produce
related outputs, but that the side-effects of the function preserve relations.
This has a number of consequences in practice:
• When replacing one implementation with another, we must ensure that
the side-effects of the two implementations are also equivalent.
• When using abstraction to preserve an invariant, we must also ensure that
the side effects preserve that invariant.
• When interpreting a “free theorem” we must consider the possible affect
of side-effects on a function’s behaviour.
94 CHAPTER 7. PARAMETRICITY
For example, whilst we do not know that all functions of type ∀𝛼.𝛼 → 𝛼 are
the identity function, we do know that if such a function returns a value then
it will be equal to the function’s input.
7.4.2 Non-parametric values
Abstraction and parametricity only hold if there are no non-parametric poly-
morphic functions available in the environment.
For example, applying parametricity to the type ∀𝛼.𝛼 → 𝛼 → Bool gives us
the following formula:
∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼 → Bool).
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿. ∀𝑢′ ∶ 𝛾. ∀𝑣′ ∶ 𝛿.
𝜌(𝑢, 𝑣) ⇒ 𝜌(𝑢′, 𝑣′) ⇒
(𝑓[𝛾] 𝑢 𝑢′ =𝐵𝑜𝑜𝑙 𝑓[𝛿]𝑣𝑣′)
If we instantiate 𝜌 with the trivial relation that is always true, then we get the
following free theorem:
∀𝑓 ∶ (∀𝛼.𝛼 → 𝛼 → Bool).
∀𝛾. ∀𝛿.
∀𝑢 ∶ 𝛾. ∀𝑣 ∶ 𝛿. ∀𝑢′ ∶ 𝛾. ∀𝑣′ ∶ 𝛿.
(𝑓[𝛾] 𝑢 𝑢′ =𝐵𝑜𝑜𝑙 𝑓[𝛿]𝑣𝑣′)
This means that any parametric function of type ∀𝛼.𝛼 → 𝛼 → Bool must be a
constant function: a function that returns the same value for all inputs.
However, OCaml provides the following built-in structural equality function:
val (=) : ’ a -> ’a -> bool
Even though it has this type, it is not a constant function. This means that it
is not parametric.
The existence of this function and several similar ones in OCaml, can break
the guarantees provided by abstraction and parametricity. However, not all
guarantees are broken, for instance the preservation of invariants is not affected
by any of the built-in functions available in OCaml.
In practice, this means that such functions should only be used at known
types. Using them on abstract types produces non-parametric code whose cor-
rectness may rely on details of an implementation that are not exposed in its
interface.