Why is there only one possible implementation of the *id* function?

Question

I have seen multiple times the claim that one can proof that a function with type signature

α → α

can only be implemented by returning the argument, because we don't know anything about the type of the parameter.

id :: α → α
id a = a

An exmample of that claim can be found at http://blog.precog.com/?p=431

But what is keeping us from making an if statement like this (pseudo code)?

id :: α → α
id a = if ( a is_a_String) a + "hello"
       else a

Is there a precondition that I'm missing?

Answer 1

Theorems like that only hold in languages that have the parametricity property. That means that code cannot inspect types at runtime, and consequently, execution can never rely on type information. Most functional languages have this property, while OO languages often see the need to provide downcasts and similar features, which break parametricity.

Parametricity is a very powerful property. It ensures certain abstraction properties, so-called "free theorems" like the one you mention, and it is the enabler for an efficient implementation that can erase types at runtime.

See also my answer here.