Names For Free: Polymorphic Views of Names and Binders

Nicolas Pouillard, Jean-Philippe Bernardy

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

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.
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
Pages13-24
ISBN (Print)978-1-4503-2383-3
DOIs
Publication statusPublished - 23 Sep 2013

Keywords

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

Fingerprint

Dive into the research topics of 'Names For Free: Polymorphic Views of Names and Binders'. Together they form a unique fingerprint.

Cite this