Names For Free: Polymorphic Views of Names and Binders

Nicolas Pouillard, Jean-Philippe Bernardy

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstrakt

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.
OriginalsprogEngelsk
TitelHaskell '13 Proceedings of the 2013 ACM SIGPLAN symposium on Haskell
Antal sider12
ForlagAssociation for Computing Machinery
Publikationsdato23 sep. 2013
Sider13-24
ISBN (Trykt)978-1-4503-2383-3
DOI
StatusUdgivet - 23 sep. 2013

Fingeraftryk

Dyk ned i forskningsemnerne om 'Names For Free: Polymorphic Views of Names and Binders'. Sammen danner de et unikt fingeraftryk.

Citationsformater