Abstracts.2020.Parametricity

Parametricity

by Andreas Abel

Abstract

We have a look at parametricity, continuing last week's topic of logical relation.

• parametric polymorphism (System F)
• relational semantics via logical relations
• "theorems for free"

The relational semantics allows us to prove properties of polymorphic functions, e.g. that any total function of type forall a. a -> a is the identity.

Material

• Formalization in Agda

Bibliography

1. John C. Reynolds. Types, Abstraction and Parametric Polymorphism. IFIP Congress 1983, pp. 513–523.
2. Philip Wadler. Theorems for Free! FPCA 1989, pp. 347–359.

Related Talks

1. Frederik Folkmar Ramcke, Theorems for free
2. Andrea Vezzosi, Parametricity for Dependent Types