Journal of Functional Programming

Articles

Proofs for free

Parametricity for dependent types

JEAN-PHILIPPE BERNARDYa1, PATRIK JANSSONa1 and ROSS PATERSONa2

a1 Chalmers University of Technology & University of Gothenburg, Sweden (e-mail: bernardy@chalmers.se, patrikj@chalmers.se)

a2 City University, London, UK (e-mail: ross@soi.city.ac.uk)

Abstract

Reynolds' abstraction theorem (Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism, Inf. Process. 83(1), 513–523) shows how a typing judgement in System F can be translated into a relational statement (in second-order predicate logic) about inhabitants of the type. We obtain a similar result for pure type systems (PTSs): for any PTS used as a programming language, there is a PTS that can be used as a logic for parametricity. Types in the source PTS are translated to relations (expressed as types) in the target. Similarly, values of a given type are translated to proofs that the values satisfy the relational interpretation. We extend the result to inductive families. We also show that the assumption that every term satisfies the parametricity condition generated by its type is consistent with the generated logic.

(Online publication March 30 2012)