Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

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.
Original language English Haskell '13 Proceedings of the 2013 ACM SIGPLAN symposium on Haskell 12 Association for Computing Machinery 23 Sep 2013 13-24 978-1-4503-2383-3 10.1145/2503778.2503780 Published - 23 Sep 2013
Close

### Research areas

• name binding, polymorphism, parametricity, type-classes, nested types

ID: 78233646