Names for free
- 23 September 2013
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 48 (12), 13-24
- https://doi.org/10.1145/2578854.2503780
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ν.ν → Term(ɑ + ν) or ϶ν.ν x Term(ν.ν) 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
This publication has 16 references indexed in Scilit:
- Type-theory in colorPublished by Association for Computing Machinery (ACM) ,2013
- A unified treatment of syntax with bindersJournal of Functional Programming, 2012
- Proofs for freeJournal of Functional Programming, 2012
- Syntax for Free: Representing Syntax with Binding Using ParametricityLecture Notes in Computer Science, 2009
- Contextual modal type theoryACM Transactions on Computational Logic, 2008
- Applicative programming with effectsJournal of Functional Programming, 2007
- A formalization of the strong normalization proof for System F in LEGOPublished by Springer Science and Business Media LLC ,2006
- The view from the leftJournal of Functional Programming, 2004
- de Bruijn notation as a nested datatypeJournal of Functional Programming, 1999
- Substitution: A formal methods case study using monads and transformationsScience of Computer Programming, 1994