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

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.

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.

StackExchange Computer Science Q#82626, answer score: 32