Parametric compositional data types

TY - GEN

T1 - Parametric compositional data types

AU - Bahr, Patrick

AU - Hvitved, Tom

N1 - Conference code: 4

PY - 2012/2/11

Y1 - 2012/2/11

N2 - In previous work we have illustrated the benefits that compositional data types (CDTs) offer for implementing languages and in general for dealing with abstract syntax trees (ASTs). Based on Swierstra's data types à la carte, CDTs are implemented as a Haskell library that enables the definition of recursive data types and functions on them in a modular and extendable fashion. Although CDTs provide a powerful tool for analysing and manipulating ASTs, they lack a convenient representation of variable binders. In this paper we remedy this deficiency by combining the framework of CDTs with Chlipala's parametric higher-order abstract syntax (PHOAS). We show how a generalisation from functors to difunctors enables us to capture PHOAS while still maintaining the features of the original implementation of CDTs, in particular its modularity. Unlike previous approaches, we avoid so-called exotic terms without resorting to abstract types: this is crucial when we want to perform transformations on CDTs that inspect the recursively computed CDTs, e.g. constant folding.

AB - In previous work we have illustrated the benefits that compositional data types (CDTs) offer for implementing languages and in general for dealing with abstract syntax trees (ASTs). Based on Swierstra's data types à la carte, CDTs are implemented as a Haskell library that enables the definition of recursive data types and functions on them in a modular and extendable fashion. Although CDTs provide a powerful tool for analysing and manipulating ASTs, they lack a convenient representation of variable binders. In this paper we remedy this deficiency by combining the framework of CDTs with Chlipala's parametric higher-order abstract syntax (PHOAS). We show how a generalisation from functors to difunctors enables us to capture PHOAS while still maintaining the features of the original implementation of CDTs, in particular its modularity. Unlike previous approaches, we avoid so-called exotic terms without resorting to abstract types: this is crucial when we want to perform transformations on CDTs that inspect the recursively computed CDTs, e.g. constant folding.

U2 - 10.4204/EPTCS.76.3

DO - 10.4204/EPTCS.76.3

M3 - Article in proceedings

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 3

EP - 24

BT - Proceedings Fourth Workshop on Mathematically Structured Functional Programming

A2 - Chapman, James

A2 - Levy, Paul Blain

PB - Open Publishing Association

T2 - 4th Workshop on Mathematically Structured Functional Programming

Y2 - 25 March 2012 through 25 March 2012

ER -