Formal parametric polymorphism

摘要

A polymorphic function is parametric if its behavior does notdepend on the type at which it is instantiated. Starting with Reynolds'work, the study of parametricity is typically semantic. In this paper,we develop a syntactic approach to parametricity, and a formal systemthat embodies this approach: system R. Girard's system F deals with terms and types;R is an extension of F that deals also with relationsbetween types.

In R**, it is possible to derive theorems about functionsfrom their types, or "theorems for free", as Wadler callsthem. An easy "theorem for free"

asserts that the type ∀XX→Bool contains only constantfunctions; this is not provable in F. There are many harder and moresubstantial examples. Various metatheoremscan also be obtained, such asa syntactic version of Reynolds' abstraction theorem.