Archive for the 'Parametricity' Category

Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism

By Geoffrey Washburn and Stephanie Weirich, from ICFP 2003, available from Stephanie Weirich’s website:

Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky routines dealing with variables, such as capture avoiding substitution. However, despite the advantages this technique provides, it is not commonly used because it is difficult to write sound elimination forms (such as folds or catamorphisms) for higher-order abstract syntax. To fold over such a data type, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the data type are parametric. In this paper, we show how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we implement a library of iteration operators over data structures containing functionals. From this implementation, we derive “fusion laws” that functional programmers may use to reason about the iteration operator. Finally, we show how this use of parametric polymorphism corresponds to the Schürmann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound and complete encoding of their calculus into System F. This encoding can serve as a starting point for reasoning about higher-order structures in polymorphic languages.

Syntax for free: representing syntax with binding using parametricity

Robert Atkey, from TLCA 2009, available from Robert Atkey’s website.

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.

Slides from the TLCA presentation are available here.