Book contents
- Frontmatter
- Contents
- Preface
- Miscellaneous Frontmatter
- Computational comonads and intensional semantics
- Weakly distributive categories
- Sequentiality and full abstraction
- Remarks on algebraically compact categories
- Dinaturality for free
- Simply typed and untyped lambda calculus revisited
- Modelling reduction in confluent categories
- On clubs and data-type constructors
- Penrose diagrams and 2-dimensional rewriting
- Strong monads, algebras and fixed points
- Semantics of local variables
- Using fibrations to understand subtypes
- Reasoning about sequential functions via logical relations
- I-categories and duality
- Geometric theories and databases
- Partial products, bagdomains and hyperlocal toposes
Simply typed and untyped lambda calculus revisited
Published online by Cambridge University Press: 24 September 2009
- Frontmatter
- Contents
- Preface
- Miscellaneous Frontmatter
- Computational comonads and intensional semantics
- Weakly distributive categories
- Sequentiality and full abstraction
- Remarks on algebraically compact categories
- Dinaturality for free
- Simply typed and untyped lambda calculus revisited
- Modelling reduction in confluent categories
- On clubs and data-type constructors
- Penrose diagrams and 2-dimensional rewriting
- Strong monads, algebras and fixed points
- Semantics of local variables
- Using fibrations to understand subtypes
- Reasoning about sequential functions via logical relations
- I-categories and duality
- Geometric theories and databases
- Partial products, bagdomains and hyperlocal toposes
Summary
Abstract
In [6] one finds a general method to describe various (typed) λ-calculi categorically. Here we give an elementary formulation in terms of indexed categories of the outcome of applying this method to the simply typed λ-calculus. It yields a categorical structure in which one can describe exponent types without assuming cartesian product types. Specializing to the “monoid” case where one has only one type yields a categorical description of the untyped λ-calculus.
In the literature there are two categorical notions for the untyped λ-calculus: one by Obtulowicz and one by Scott & Koymans. The notion we arrive at subsumes both of these; it can be seen as a mild generalization of the first one.
Introduction
The straightforward way to describe the simply typed λ-calculus (denoted here by λ1) categorically is in terms of cartesian closed categories (CCC's), see [10]. On the type theoretic side this caused some discomfort, because one commonly uses only exponent types without assuming cartesian product types — let alone unit (i.e. terminal) types. The typical reply from category theory is that one needs cartesian products in order to define exponents. Below we give a categorical description of exponent types without assuming cartesian product types. We do use cartesian products of contexts; these always exist by concatenation. Thus both sides can be satisfied by carefully distinguishing between cartesian products of types and cartesian products of contexts. We introduce an appropriate categorical structure for doing so.
In [6] one can find a general method to describe typed λ-calculi categorically. One of the main organizing principles used there is formulated below. It deserves the status of a slogan.
- Type
- Chapter
- Information
- Applications of Categories in Computer ScienceProceedings of the London Mathematical Society Symposium, Durham 1991, pp. 119 - 142Publisher: Cambridge University PressPrint publication year: 1992
- 4
- Cited by