# How exactly do we define parametric polymorphism?

My naive distinction between parametric polymorphism and ad-hoc polymorphism, is that:

In parametric polymorphism, the type is given as a variable: (pseudocode)

Function f: <.Type T> T $$\to$$ T {...}

Whereas in ad-hoc polymorphism, we write different functions for each type:

Function f: Int $$\to$$ Int {...}

Function f: Bool $$\to$$ Bool {...}

But by that definition, we can always “pretend” to do parametric polymorphism:

Function f: <.Type T> T $$\to$$ T { if T == Int then {...}; If T == Bool then {...} }

How exactly do we define, from a type theory standpoint, parametric polymorphism, so that this is not allowed? Do we simply say that the term T is not allowed to be used in the body of $$f$$?

An informal, but better way of explaining parametric polymorphism is that the term has a uniform definiton/semantics for all types. A simple example is the identity function:

$$λ x. x$$

This is one term that can be reasonably given the type $$ℕ → ℕ$$, $$\mathsf{Bool} → \mathsf{Bool}$$, etc. Therefore, we also consider it reasonable for it to give it the type $$∀a. a → a$$, because it is a single term that works for every type.

If you want to talk about terms where types are explicitly talked about, then this becomes somewhat less clear. However, an informal idea of what must be going on in those definitions is that the type variables are completely unknown to the definition. So in:

$$Λa. λ(x : a). x$$

even though we get syntactically different terms for each choice of $$a$$, the definition didn't specify what happens for particular choices of $$a$$, or something of that sort.

The more formal/precise way of explaining all of this is usually relational parametricity. That's kind of complicated to get into, but it says that there are ways of interpreting our definitions into relations in addition to the normal semantics. In this explanation, parametric polymorphism is about preserving relatedness. So, if you instantiate a polymorphic value to related types, the values you get are related in a coherent way. And the reason why relations are used is that they give a precise (but general) way of talking about what it means for things to be 'uniform' like above.

Contrary to what you wrote, in many languages with parametric polymorphism, the type usually is not provided as an argument to the function. At least, it's not like the other arguments. You can't write something like "if T == int ..." because T is not a variable that can you can access in this way.

(How can you ensure this separation between arguments vs types? One way is to have type variables and data variables. Data variables can be used in computation, and type variables can be used to describe the type of data variables and expressions and function arguments, but computation can't access the contents of type variables or branch on them.)

• very clarifying. So essentially, in this set-up, the types ONLY have the purpose of checking whether your program is a syntactically correct program? It's essentially only a restriction on the programs you're allowed to write, but as soon as the program is written, the types have no influence on the computation? – user56834 Mar 3 '19 at 20:11
• @user56834, yes, exactly! You stated it better than I was able to. Thank you for finding such a clean summary of what I was trying to get at. (Standard caveat: there are many programming languages, and each one does something a little different, so I'm trying to describe what is the most common situation. I'm sure there are exceptions.) – D.W. Mar 3 '19 at 20:40
• @user56834 Indeed. That property is related to "type erasure": if we have parametric polymorphism, at runtime we do not need any type information, so we can save memory omitting types everywhere. One could implement the language essentially passing bare pointers everywhere (e.g. void * in C), which are guaranteed to be safely used by the type system. Static type checks provide this guarantee with zero runtime overhead. – chi Mar 4 '19 at 11:16
• @chi, thanks for relating the term "type erasure" to this so I can google it. – user56834 Mar 4 '19 at 11:53

A useful intuition is the one you described: the code of a parametric-polymorphic function f can not access type T and choose to behave in different ways according to what T is.

Essentially, for f the values of type T are opaque: f can interact with those values only in very restricted ways. For instance, f can "move them around":

f : <T,U> (T,U) -> (U,T)
f (t,u) = (u,t)


Here, f swaps the pair "moving" their components, but does not really interact with those.

Function f can also interact with the values exploiting its arguments

f : <T> (T, T->Bool) -> Int
f (t,g) = if g(t) then 4 else 6


Here f interacts with t, but only through function g which is passed as an argument.

A precise formalization of the behavior of functions whose behavior (roughly) does not "depend on T" was given by Reynolds when he studied parametricity and proved the abstraction theorem. This is a bit complex in the general case, but one can grasp some ideas from the following example.

Let List(T) denote a type for finite sequences of values [t1,...,tn] of type T. In particular, given any function g : T -> U, we can "lift" this to lists and obtain map g : List(T) -> List(U) by letting

map g([t1,...,tn]) = [g(t1),...,g(tn)]


For instance, if g : Int -> Int is defined as g(n)=n+1, then map g : List(Int) -> List(Int) will increment each value of its input: map g([x1,..,xn]) = [x1+1,...,xn+1].

Finally, consider a parametric-polymorphic function

f : <A> List(A) -> List(A)


and assume that, when A = Int we have

f<Int> ([1,2,3]) = [2,1,1]


Now, recall f is parametric-polymorphic. So, f did not really "know" that 1 was number one -- it did not even "know" it was an integer. Consequently, if we replace 1 with any value x, 2 with any value y and 3 with any value z, all of type T function f has to satisfy

f<T> ([x,y,z]) = [y,x,x]


This can be further generalized as follows:

for any g : T -> U
f<U> (map g(list)) = map g(f<T> (list))


which reads as: if we affect the elements of the input list elements using g before calling f, we get the same result as calling f first, and then affect the output list elements using g. Intuitively, this has to be the case, since f can not "read" the elements, but can only "move them around", "duplicate them", or "discard them".

(In category theory, that's called a "naturality property")

Note that, in virtue of the above property, if we need to test a list-reversal parametric-polymorphic function

reverse : <T> List(T) -> List(T)


we can simply choose T = Int, and test for lists of integers [1,2,...,n], only. That's because if the function reverses those lists of integers, it will reverse any other list (even those having a different element type).

You may want to convince yourself that the above property can be generalized to all "cointainer" types (lists, pairs, trees, ...). Parametricity goes beyond that, but that's a good example in my mind.

The "theorems for free!" paper by Wadler is a classic introduction to parametricity and contains further examples.

• Thank you! this clarifies. What I noticed in your answer, which I didn't quite notice when I read through the "theorems for free!" paper yesterday, is that the behaviour of the function $\text{map } g$ in your answer seems to be essential to the "parametricity" of $f$. Really it seems to me that it's not enough for $f$ to be parametric, $\text{map } g$ ALSO needs to be "parametric". I am not sure if I'm using the terms correctly now? But the point is, $\text{map}$ can not use any information about the type $T$ either, right? In categorical terms, we need the "functor to be parametric" as well? – user56834 Mar 4 '19 at 12:18
• I'm not sure how to state it correctly, but we for example cannot have: $\text {map }g([t_1,...t_n])=[g(t_1),...,h(t_1)]$ where $h(x)$ is some other function. This would violate "parametricity" of the functor $\text{map } g$. (please tell me if this is correct and whether I'm using the terms correctly) – user56834 Mar 4 '19 at 12:22
• @user56834 Technically, a functor comprises both a type-level function (T to List(T)) and an application map turning g into map g, satisfying certain laws (the functor laws). Your alternative map g indeed does NOT satisfy those laws. Usually map g can be defined within the programming language itself, so it's parametric. In theory, often we simply consider a few standard functors (constant, diagonal, identity, product, coproduct, ...) each of which come with a "parametric" map (which can be defined in the language). Composing those functors then simply works fine. – chi Mar 4 '19 at 13:04
• @user56834 Because of this, we usually do not require that map g is parametric. The functor laws suffice to rule out unwanted maps. – chi Mar 4 '19 at 13:06