Names For Free: Polymorphic Views of Names and Binders

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

View graph of relations

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 languageEnglish
Title of host publicationHaskell '13 Proceedings of the 2013 ACM SIGPLAN symposium on Haskell
Number of pages12
PublisherAssociation for Computing Machinery
Publication date23 Sep 2013
ISBN (Print)978-1-4503-2383-3
Publication statusPublished - 23 Sep 2013

    Research areas

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

ID: 78233646