Abstract
We propose a novel technique to represent names and binders in
Haskell. The dynamic (run-time) representation is based on de Bruijn
indices, but it features an interface to write and manipulate
variables conviently, using Haskell-level lambdas and variables. The
key idea is to use rich types: a subterm with an additional free variable
is viewed either as $\forall v. v \rightarrow \mathsf{Term} (a + v)$
or $\exists v. v \times \mathsf{Term} (a + v)$ depending on whether it
is constructed or analysed. We demonstrate on a number of examples how
this approach permits to express term construction and manipulation in
a natural way, while retaining the good properties of representations
based on de Bruijn indices.
Haskell. The dynamic (run-time) representation is based on de Bruijn
indices, but it features an interface to write and manipulate
variables conviently, using Haskell-level lambdas and variables. The
key idea is to use rich types: a subterm with an additional free variable
is viewed either as $\forall v. v \rightarrow \mathsf{Term} (a + v)$
or $\exists v. v \times \mathsf{Term} (a + v)$ depending on whether it
is constructed or analysed. We demonstrate on a number of examples how
this approach permits to express term construction and manipulation in
a natural way, while retaining the good properties of representations
based on de Bruijn indices.
| Original language | English |
|---|---|
| Title of host publication | Haskell '13 Proceedings of the 2013 ACM SIGPLAN symposium on Haskell |
| Number of pages | 12 |
| Publisher | Association for Computing Machinery |
| Publication date | 23 Sept 2013 |
| Pages | 13-24 |
| ISBN (Print) | 978-1-4503-2383-3 |
| DOIs | |
| Publication status | Published - 23 Sept 2013 |
Keywords
- name binding, polymorphism, parametricity, type-classes, nested types