How exactly do we define parametric polymorphism?

Question

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$?

The reason I’m asking is: I am reading about the fact that parametric polymorphism allows certain nice guarantees that ad-hoc polymorphism doesn’t.

Answer 1

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.

Answer 2

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.)

Answer 3

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.