Parametricity of the polymorphic lambda calculus
This is a formalization of the polymorphic lambda calculus (System F) with a proof of Reynolds's parametricity theorem.
The formalization uses a dependently-typed representation, which ensures that all terms are well-typed by construction. This enables a natural style of denotational semantics.
References
- Types, Abstraction and Parametric Polymorphism, by John C. Reynolds, IFIP 1983.
- Theorems for free!, by Philip Wadler, ICFP 1989.
Highlights
Syntax
Types
(**
<<
t ::= t -> t (* Function *)
| forall t (* Type generalization *)
| i (* Type variable (DeBruijn index) *)
| unit (* Unit type *)
| t * t (* Product *)
| t + t (* Sum *)
>>
*)
Inductive ty (n : nat) : Type :=
| Arrow : ty n -> ty n -> ty n
| Forall : ty (S n) -> ty n
| Tyvar : bnat n -> ty n
(* Basic data types *)
| Unit : ty n
| Prod : ty n -> ty n -> ty n
| Sum : ty n -> ty n -> ty n
.Terms
(**
<<
u ::= tyfun u (* Type abstraction *)
| fun u (* Value abstraction *)
| u u (* Application *)
| i (* Variable *)
| c (* Constant *)
>>
*)
Inductive tm (n : nat) (vs : list (ty n)) : ty n -> Type :=
| TAbs {t}
: tm (S n) (map (shift_ty 0) vs) t ->
tm n vs (Forall t)
| Abs {t1 t2}
: tm n (t1 :: vs) t2 ->
tm n vs (Arrow t1 t2)
| App {t1 t2}
: tm n vs (Arrow t1 t2) ->
tm n vs t1 ->
tm n vs t2
| Var (v : bnat (length vs))
: tm n vs (lookup_list vs v)
| Con {t}
: cn t ->
tm n vs t
.Semantics
Signatures of the denotation functions.
Simplified versions, where tm0 is tm specialized to the empty context
(n = 0 and vs = []).
(** Semantics of types as Coq types *)
Definition eval_ty0 : ty 0 -> Type.
(** Semantics of terms as Coq values *)
Definition eval_tm0 {t : ty 0} : tm0 t -> eval_ty0 t.
(** Relational semantics of types *)
Definition eval2_ty0 (t : ty 0) : eval_ty0 t -> eval_ty0 t -> Prop.Parametricity theorem
(** For any term [u] of type [t], the interpretation of [u] ([eval_tm0 u])
satisfies the relational interpretation of [t] ([eval2_ty t]). *)
Theorem parametricity0 (t : ty 0) (u : tm0 t)
: eval2_ty0 t (eval_tm0 u) (eval_tm0 u).