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

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.

StackExchange Computer Science Q#105062, answer score: 5