Nested Datatypes

By Richard S. Bird, Lambert G. L. T. Meertens. 1998

How researchers see this paper

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

1. Ralph Matthes
2. Tarmo Uustalu
3. Benedikt Ahrens

Citations in the corpus

• Heterogeneous substitution systems revisited (2016, neutral): “This is the general situation of the “gfolds” of Bird and Paterson [13], and (the carriers of) the corresponding initial F -algebras are called “nested datatypes” [11].”
• de Bruijn notation as a nested datatype (1999, background): “…may be represented as the following element of Term Char: Lam (Lam (App (App (Var (Succ Zero),Var Zero),Var (Succ (Succ ‘z’))))) The type Term is an example of a nested datatype (Bird and Meertens, 1998) because its definition has a recursive use with a different argument from the left-hand side.”
• Iteration and coiteration schemes for higher-order and nested datatypes (2005, background): “The second line defines “bushes” [10] which are like lists except that the element type gets bigger as we are traversing the list from head to tail.”
• Map fusion for nested datatypes in intensional type theory (2011, background): “Also for nested datatypes, laws have been important from the beginning [1].”
• Extended Initiality for Typed Abstract Syntax (2011, unknown): “We give a possibly non–exhaustive list of techniques for binder representation: (1) Nominal syntax using named abstraction; (2) Higher–Order Abstract Syntax (HOAS), e.g. lam : ( T → T ) → T and its weak variant, e.g. lam : ( var → T ) → T ; (3) Nested datatypes as presented in [BM98].”
• Substitution in Non-wellfounded Syntax with Variable Binding (2003, background): “(recursive constructors of rank 2) is currently on the research agenda, see [10,11,22,31] .”