Why must a function with polymorphic type `forall t: Type, t->t` be the identity function?

Question

I am new to programming language theory. I was watching some online lectures in which the instructor claimed that a function with polymorphic type forall t: Type, t->t be the identity, but did not explain why. Can someone explain to me why? Maybe a proof of the claim from first principles.

Answer 1

The first thing to note is that this isn't necessarily true. For example, depending on the language a function with that type, besides being the identity function, could: 1) loop forever, 2) mutate some state, 3) return null, 4) throw an exception, 5) perform some I/O, 6) fork a thread to do something else, 7) do call/cc shenanigans, 8) use something like Java's Object.hashCode, 9) use reflection to determine if the type is an integer and increment it if so, 10) use reflection to analyze the call stack and do something based on the context within which it is called, 11) probably many other things and certainly arbitrary combinations of the above.

So the property that leads to this, parametricity, is a property of the language as a whole and there are stronger and weaker variations of it. For many of the formal calculi studied in type theory, none of the above behaviors can occur. For example, for System F/the pure polymorphic lambda calculus, where parametricity was first studied, none of the above behaviors above can occur. It simply doesn't have exceptions, mutable state, null, call/cc, I/O, reflection, and it's strongly normalizing so it can't loop forever. As Gilles mentioned in a comment, the paper Theorems for free! by Phil Wadler is a good introduction to this topic and its references will go further into the theory, specifically the technique of logical relations. That link also lists some other papers by Wadler on the topic of parametricity.

Since parametricity is a property of the language, to prove it requires first formally articulating the language and then a relatively complicated argument. The informal argument for this particular case assuming we're in the polymorphic lambda calculus is that since we know nothing about t we can't perform any operations on the input (e.g. we can't increment it because we don't know if it is a number) or create a value of that type (for all we know t=Void, a type with no values at all). The only way to produce a value of type t is to return the one that is given to us. No other behaviors are possible. One way to see that is to use strong normalization and show that there is only one normal form term of this type.

Answer 2

The proof of the claim is quite complex, but if that's what you really want, you can check out Reynolds' original paper on the topic.

The key idea is that it holds for parametrically polymorphic functions, where the body of a polymorphic function is the same for all monomorphic instantiations of the function. In such a system, no assumptions can be made about the type of a parameter of polymorphic type, and if the only value in scope has a generic type, there's nothing to do with it but return it, or pass it to other functions you've defined, that can in turn do nothing but return it or pass it.. .etc. So in the end, all you can do is some chain of identity functions before returning the parameter.

Answer 3

With all the caveats that Derek mentions, and ignoring paradoxes that result from using set theory, let me sketch a proof in the spirit of Reynolds/Wadler.

A function of the type:

f :: forall t . t -> t

is a family of functions $f_t$ indexed by type $t$.

The idea is that, to formally define polymorphic functions, we should not treat types as sets of values, but rather as relations. Basic types, like Int induce equality relations--e.g., two Int values are related if they are equal. Functions are related if they map related values to related values. The interesting case is polymorphic functions. They map related types to related values.

In our case, we want to establish a relation between two polymorphic functions $f$ and $g$ of the type:

forall t . t -> t

Suppose that type $s$ is related to type $t$. The first function $f$ maps type $s$ to a value--here, the value itself is a function $f_s$ of the type $s \to s$. The second function maps type $t$ to another value $g_t$ of the type $t \to t$. We say that $f$ is related to $g$ if the values $f_s$ and $g_t$ are related. Since these values are themselves functions, they are related if they map related values to related values.

The crucial step is to use the Reynolds' parametricity theorem, which says that any term is in a relation with itself. In our case, the function f is related to itself. In other words, if s is related to t, $f_s$ is also related to $f_t$.

We can now pick any relation between any two types and apply this theorem. Let's pick the first type as the unit type (), which has only one value, also called (). We'll keep the second type t arbitrary but non-empty. Let's pick a relation between () and t to be simply one pair ((), c), where c is some value of the type t (a relation is just a subset of the cartesian product of sets). Parametricity theorem tells us that $f_{(\,)}$ must be related to $f_t$. They must map related values to related values. The first function $f_{(\,)}$ doesn't have much choice, it must map the only value () back to (). Therefore the second function $f_t$ must map c to c (the only values related to ()). Since c is completely arbitrary, we conclude that $f_t$ is $id_t$ and, since t is completely arbitrary, f is id.

You can find more details in my blog.

Answer 4

EDIT: A comment above has provided the missing piece. Some people are deliberately playing with less-than-turing-complete languages. I explicitly don't care about such languages. A really usuable not-turing-complete language is a crazy hard thing to design. The whole rest of this expands on what happens trying to apply these theorems to a full language.

False!

function f(a): forall t: Type, t->t
    function g(a): forall t: Type, t->t
       return (a is g) ? f : a
    return a is f ? g : a

where the is operator compares two variables for reference identity. That is, they contain the same value. Not an equivalent value, same value. Functions f and g are equivalent by some definition but they aren't the same.

If this function is passed itself it returns something else; otherwise it returns its input. The something else has the same type as itself therefore it can be substituted. In other words, f is not the identity, because f(f) returns g, whereas the identity would return f.

For the theorem to hold it has to assume the ridiculous ability to reduce

function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(1000, <0, a>)[1]¹

If you're willing to assume that you can assume the much easier type inference can be handled.

If we try to restrict the domain until the theorem holds we end up having to restrict it awfully far.

• Pure Functional (no mutable state, no IO). OK I can live with that. A lot of time we want to run proofs over functions.
• Empty standard library. meh.
• No raise and no exit. Now we're starting to get constrained.
• There is no bottom type.
• The language has a rule that allows the compiler to collapse infinite recursion by assuming it must terminate. The compiler is allowed to reject trivial infinite recursion.
• The compiler is allowed to fail if presented with something that can't be proved either way.² Now the standard library can't take functions as arguments. Boo.
• There is no nil. This is starting to get problematic. We've ran out of ways to deal with 1/0.³
• The language can't do branch type inferences and does not have an override for when the programmer can prove a type inference the language cant. This is pretty bad.

The existence of both of the last two constraints has crippled the language. While it is still Turing complete the only way to get general purpose work out of it is to simulate an inner platform that interprets a language with looser requirements.

¹ If you think the compiler can deduce that one, try this one

function fermat(z) : int -> int
    function pow(x, p)
        return p = 0 ? 1 : x * pow(x, p - 1)
    function f2(x, y, z) : int, int, int -> <int, int>
        left = pow(x, 5) + pow(y, 5)
        right = pow(z, 5)
        return left = right
            ? <x, y>
            : pow(x, 5) < right
                ? f2(x + 1, y, z)
                : pow(y, 5) < right
                    ? f2(2, y + 1, z)
                    : f2(2, 2, z + 1)
    return f2(2, 2, z)
function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(fermat(3)[0], <0, a>)[1]

² The proof that the compiler can't do this depends on blinding. We can use multiple libraries to ensure the compiler can't see the loop at once. Also, we can always construct something where the program would work but could not be compiled because the compiler can't perform the induction in available memory.

³ Somebody thinks you can have this return nil without arbitrary generic types returning nil. This pays a nasty penalty for which I have seen no effective language that can pay it.

function f(a, b, c): t: Type: t[],int,int->t
    return a[b/c]

must not compile. The fundamental problem is runtime array indexing doesn't work anymore.