Parametric Polymorphic Representations of Syntax with Binding

bob.atkey@ed.ac.uk Return to my homepage

This page collects together my work on parametricity. In particular, the use of parametric polymorphism to represent syntax with binding using higher-order abstract syntax.

• Robert Atkey. A Deep Embedding of Parametric Polymorphism in Coq. Workshop on Mechanizing Metatheory. 2009.
  We describe a deep embedding of System F inside Coq, along with a denotational semantics that supports reasoning using Reynolds parametricity. The denotations of System F types are given exactly by objects of sort Set in Coq, and the relations used to formalise Reynolds parametricity are Coq predicates with values in Prop. A key feature of the model is the extensive use of dependent types to maintain agreement between the parts of the model. We use type dependency to represent well-formedness of types and terms, and to keep track of the relation between the denotations of types and the parametricity relations between them.
• Robert Atkey. Syntax For Free: Representing Syntax with Binding using Parametricity. In Typed Lambda Calculi and Applications, TLCA 2009, volume 5608 of Lecture Notes in Computer Science, pages 35—49. Springer, 2009.
  We show that, in a parametric model of polymorphism, the type ∀α. ((α → α) → α) → (α → α → α) → α is isomorphic to closed deBruijn terms. That is, the type of closed higher-order abstract syntax terms is isomorphic to a concrete representation. To demonstrate the proof we have constructed a model of parametric polymorphism inside the Coq proof assistant. The proof of the theorem requires parametricity over Kripke relations. We also investigate some variants of this representation.

Most of the proofs in the paper have been formalised in the Coq proof assistant. This development, and an additional demonstration file in OCaml are available here. This development needs Coq version 8.2 to compile. The Coqdoc documentation is also available.

See also an application of this work in the Haskell programming language: Unembedding Domain-Specific Languages.