Simply typed and untyped lambda calculus revisited
Bart Jacobs · Cambridge University Press eBooks · 1992
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.