Syntax for free: Representing syntax with binding using parametricity

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. © 2009 Springer Berlin Heidelberg.