Monadic Presentations of Lambda Terms Using Generalized Inductive Types
By Thorsten Altenkirch, Bernhard Reus. 1999
We present a definition of untyped λ-terms using a heterogeneous datatype, i.e. an inductively defined operator. This operator can be extended to a Kleisli triple, which is a concise way to verify the substitution laws for λ-calculus. We also observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. We extend the construction to the simply typed λ-calculus using dependent types, and show that this is an instance of a generalization of Kleisli triples. The proofs for the untyped case have been checked using the LEGO system.
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
- Ralph Matthes
- Karthikeyan Bhargavan
- Andreas Abel
- Tarmo Uustalu
- Cédric Fournet
- Antoine Delignat-Lavaud
- James Chapman
- Nikhil Swamy
Citations in the corpus
- 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].”
- 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”
- Monads need not be endofunctors (2010, methodology): “[8] T. Altenkirch and B. Reus.”
- Dependent types and multi-monadic effects in F* (2016, background): “This idea was originally proposed by Altenkirch and Reus (1999).”
- 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 Linearity (2006, background): “With these notations, glueing yields nil : ∗ [1] −→ L, cons : L[1] × L −→ L where ∗ denotes the final functor in the category of endofunctors of Setτ .”
- Iteration and coiteration schemes for higher-order and nested datatypes (2005, methodology): “as in the structurally inductive approach in Altenkirch and Reus [5]:”
- Extended Initiality for Typed Abstract Syntax (2011, unknown): “2.9), as exhibited by Altenkirch and Reus [AR99].”