Names For Free: Polymorphic Views of Names and Binders

Nicolas Pouillard; Jean-Philippe Bernardy

doi:10.1145/2503778.2503780

Names For Free: Polymorphic Views of Names and Binders

Nicolas Pouillard
, Jean-Philippe Bernardy

Programming Logic and Semantics

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-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 language	English
Title of host publication	Haskell '13 Proceedings of the 2013 ACM SIGPLAN symposium on Haskell
Number of pages	12
Publisher	Association for Computing Machinery
Publication date	23 Sept 2013
Pages	13-24
ISBN (Print)	978-1-4503-2383-3
DOIs	https://doi.org/10.1145/2503778.2503780
Publication status	Published - 23 Sept 2013

Keywords

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

Access to Document

10.1145/2503778.2503780

http://dl.acm.org/citation.cfm?id=2503780

Cite this

@inproceedings{7e3d368376134ff887039a4d1c8b0297,

title = "Names For Free: Polymorphic Views of Names and Binders",

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 \$\textbackslash{}forall v. v \textbackslash{}rightarrow \textbackslash{}mathsf\{Term\} (a + v)\$ or \$\textbackslash{}exists v. v \textbackslash{}times \textbackslash{}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. ",

keywords = "name binding, polymorphism, parametricity, type-classes, nested types, name binding, polymorphism, parametricity, type-classes, nested types",

author = "Nicolas Pouillard and Jean-Philippe Bernardy",

year = "2013",

month = sep,

day = "23",

doi = "10.1145/2503778.2503780",

language = "English",

isbn = "978-1-4503-2383-3 ",

pages = "13--24",

booktitle = "Haskell '13 Proceedings of the 2013 ACM SIGPLAN symposium on Haskell",

publisher = "Association for Computing Machinery",

address = "United States",

}

TY - GEN

T1 - Names For Free

T2 - Polymorphic Views of Names and Binders

AU - Pouillard, Nicolas

AU - Bernardy, Jean-Philippe

PY - 2013/9/23

Y1 - 2013/9/23

N2 - 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.

AB - 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.

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

U2 - 10.1145/2503778.2503780

DO - 10.1145/2503778.2503780

M3 - Article in proceedings

SN - 978-1-4503-2383-3

SP - 13

EP - 24

BT - Haskell '13 Proceedings of the 2013 ACM SIGPLAN symposium on Haskell

PB - Association for Computing Machinery

ER -

Names For Free: Polymorphic Views of Names and Binders

Abstract

Keywords

Access to Document

Fingerprint

Cite this