Boxes Go Bananas: Parametric Higher-Order Abstract Syntax in System F

Stephanie Weirich
University of Pennsylvania

Monday, 5 May 2003, 2:00 PM

Lieb 3rd floor Conference Room
 

Abstract


Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by abstractions and variables in the host language. Consequently, one can avoid implementing common and tricky routines dealing with variables, such as capture-avoiding substitution. 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 datatype, one must either simultaneously define an inverse operation (which may not exist) or show that all functions embedded in the datatype are parametric.

In this talk, I will show how first-class polymorphism can be used to guarantee the parametricity of functions embedded in higher-order abstract syntax. With this restriction, we can 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 Schürmann, Despeyroux and Pfenning method of enforcing parametricity through modal types. We do so by using this library to give a sound encoding of their calculus into System F. This encoding can serve as a starting point for reasoning about higher-order structures in languages based upon System F.

This talk is based on joint work with Geoff Washburn.