The Genericity Theorem and the notion of parametricity in the polymorphic lambda-calculus

In the polymorphic �-calculus, one may explicitly define functions that take a type as input and return a term as output. This work focuses on how such functions depend on their input types. Indeed, these functions are generally understood to have an essentially constant meaning on input types. We show how the proof theory of the polymorphic �-calculus suggests a clear syntactic description of this phenomenon. Namely, under a reasonable condition, we show that if two polymorphic functions agree on an input type, then they are, in fact, the same function. Equivalently, types are generic inputs to polymorphic functions