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.
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.