Names For Free: Polymorphic Views of Names and Binders
- Nicolas Pouillard,
- Jean-Philippe Bernardy
- ,
- University of Gothenburg,
- Chalmers University of Technology
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-review
Open access
Publication Information
Output type
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 13-24 (12 pages)Publication milestones
- Published - 23/09/2013
Publication status
Published - 23/09/2013
Publisher
Association for Computing Machinery, United StatesISBN (Print)
978-1-4503-2383-3 Publication IDs
- Scopus: 84885611454
Host publication title
Haskell '13 Proceedings of the 2013 ACM SIGPLAN symposium on Haskell 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.
Publication metrics
PlumX, opens in new tab
Citations
3
Captures
6