CPL - Chalmers Publication Library

# Names For Free - Polymorphic Views of Names and Binders

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Nicolas Pouillard
ACM SIGPLAN Haskell Symposium Co-located with ICFP (0362-1340). Vol. 48 (2013), 12, p. 13-24.
[Konferensbidrag, refereegranskat]

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 weather it is constructed or analysed. We demonstrate on a number of examples how this approach approach permits to express terms construction and manipulation in a natural way, while retaining the good properties of representations based on de Bruijn indices.

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

### Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden

Denna post skapades 2013-06-17. Senast ändrad 2015-03-03.
CPL Pubid: 178606

# Läs direkt!

Länk till annan sajt (kan kräva inloggning)