de Bruijn notation as a nested datatype

By Richard S. Bird, Ross A. Paterson. 1999

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Substitution in Non-wellfounded Syntax with Variable Binding (2003, background): “The rank 2 inductive constructor representation of the untyped lambda calculus syntax in the de Bruijn version in either a functional language or a typed lambda calculus is implicit in Bellegarde and Hook [9] and appears explicated in Altenkirch and Reus [7] and Bird and Paterson [12](remarkably, Al”
Generalised folds for nested datatypes (1999, methodology): “We call such nested datatypes linear; almost all of the known practical examples of nested datatypes belong to this class. For an exception, see Section 5 of [ BP99 ].”
Initial Semantics for Strengthened Signatures (2012, background): “It is well-known [6, 3, 13] that Λ has a natural structure of cocontinuous monad where the monad composition is given by variable substitution.”
Modules over monads and initial semantics (2010, background): “The idea that the notion of monad is suited for modelling substitution concerning syntax (and semantics) is deeply rooted in the folklore and appears at least in [1, 3 ]. It has been retained by many other recent contributions concerned with syntax, although some other settings have been considered”
Map fusion for nested datatypes in intensional type theory (2011, methodology): “The basic example where variable binding is represented through a nested datatype is a typeful de Bruijn representation of untyped lambda calculus, following ideas of [4, 5, 6].”
Scrap your boilerplate: a practical design pattern for generic programming (2003, background): “Here are some typical examples (the last one is taken from [3]):”
Monadic Presentations of Lambda Terms Using Generalized Inductive Types (1999, background): “Building on this approach, in [ BP99 ] heterogeneous definitions of untyped λ-terms are investigated.”
Iteration and coiteration schemes for higher-order and nested datatypes (2005, methodology): “Whilst for a fixed hofunctorF : k2, the efficient fold “e” is of type k1F k1HG, Bird and Paterson define a generalized fold “g” of type ( k1F) ◦ H ⊆k1 G.”
A history of Haskell: being lazy with class (2007, methodology): “…possible, andoccasionally very useful, to declare data types parameterised over higher kinds, such as: data ListFunctor f a = Nil | Cons a (f a) Furthermore, one may need functions quantified over higherkinded type variables to process nested data types (Okasaki, 1999; Bird and Paterson, 1999).”