Syntax for Free: Representing Syntax with Binding Using Parametricity

Publication Information

Robert Atkey. Syntax for Free: Representing Syntax with Binding Using Parametricity. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, volume 5608 of Lecture Notes in Computer Science, 35-49. Springer, 2009.
DOI: 10.1007/978-3-642-02273-9_5

Abstract

We show that, in a parametric model of polymorphism, the type ∀𝛼. ((𝛼 → 𝛼) → 𝛼) → (𝛼 → 𝛼 → 𝛼) → 𝛼 is isomorphic to closed de Bruijn 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.

Additional Information

With Sam Lindley and Jeremy Yallop, we developed an application of the result of this paper to handling embedded domain-specific languages (EDSLs) in Haskell. This was published as a Haskell Symposium paper in 2009.

The formalisation of the model used in this paper is described in a short abstract presented at the Workshop on Mechanising Metatheory in 2009. The Coq development (tested with Coq8.4pl6) can be downloaded from the GitHub repository.