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.
| Originalsprog | Engelsk |
|---|---|
| Titel | Haskell '13 Proceedings of the 2013 ACM SIGPLAN symposium on Haskell |
| Antal sider | 12 |
| Forlag | Association for Computing Machinery |
| Publikationsdato | 23 sep. 2013 |
| Sider | 13-24 |
| ISBN (Trykt) | 978-1-4503-2383-3 |
| DOI | |
| Status | Udgivet - 23 sep. 2013 |
Emneord
- name binding, polymorphism, parametricity, type-classes, nested types