Peter LeFanu Lumsdaine: Parametricity for type theories
Time: Wed 2020-03-04 10.00 - 11.45
Location: Kräftriket, house 5, room 16
Participating: Peter LeFanu Lumsdaine
“Parametricity” refers to an important class of results and properties of type theories, especially as used in programming languages, where the consequences of parametricity are known as “free theorems”.
The classic example says that in a polymorphic type theory (e.g. System F) with list types, any polymorphic function [ f : forall A, list A —> list A ] must be *natural* in its type argument, in that for any function [ g : A —> B ], it will satisfy [ (f B) . (listmap g) = (listmap g) . (f A) ].
Technically, parametricity results are often proved using *relational* and similar models of type theories, and variants. In this expository seminar, I will survey parametricity results and their proofs for several type theories.