Abstracts.2020.STLCCC

Simply-Typed λ-Calculus and Cartesian Closed Categories

by Andreas Abel and Sandro Stucki

Two-part lecture series scheduled for Nov 5 and 12, 2020. Previously held in three parts.

Part I: Simply-Typed λ-Calculus

• Recapitulation of simply-typed λ-calculus (STLC) with product A × B and unit 1 types
• Explicit substitutions Δ ⊢ t ∘ σ : A for Γ ⊢ t : A and Δ ⊢ σ : Γ
• Equational theory Γ ⊢ t = u : A for STLC with product and unit types, and explicit substitutions. The point is that substitution was defined by inspection of the syntax of terms but is now axiomatized.
• Nameless presentation (de Bruijn style)
• Reduce de Bruijn indices n to weakenings 0 ∘ pⁿ of the first de Bruijn index 0
• Show that the set of terms Γ ⊢ t : A is in bijection with substitutions Γ ⊢ σ : ε.A, but also with functions ε.ΠΓ ⊢ f : A where ΠΓ is the left-associated iterated product type of Γ ::= ε | Γ.A. The point is that the judgement of t is asymmetric while the judgements of σ and f are symmetric, a pair of σ₁ and σ₂ or a pair of f₁ and f₂ may be composed.

Part II: Cartesian Closed Categories

• Categories: Basic definition of the algebra of functions

• Cartesian closed categories (CCCs) 𝒞 with a choice of

  • Terminal object 1 : 1 → 𝒞
  • Binary products -×- : 𝒞 × 𝒞 → 𝒞
  • Exponential/internal hom objects A→- : 𝒞 → 𝒞 for each A : 𝒞

  Note that each of these three categorical structures can be defined as "the" right adjoint to a previously defined functor, and thus both by a universal property but also purely equationally.

• The internal language of a CCC

• Implementing the internal language of a CCC in STLC with product and unit types

Notes, Exercises and Code

• Lecture notes and exercises
• Agda code

Literature

Reading on this lecture:

• Wikipedia, Curry-Howard-Lambek-Correspondence
• Andreas Abel, Lambda-Kalkül, Kapitel 7 (7.0, 7.3, 7.4) und 9 (9.0, 9.1, 9.3, 9.4) (in German)
• Jonathan Prieto-Cubides, The Simply Typed Lambda Calculus, slides: From named terms to de Bruijn terms; type-checking. Based on Agda code by gergoerdi
• Steve Awodey, Category theory, Section 6.6
• Joachim Lambek and Philip J. Scott, Introduction to higher order categorical logic

Further reading on categorical logic of typed λ-calculus:

• Simon Castellan and Pierre Clairambault and Peter Dybjer, Categories with Families: Unityped, Simply Typed, and Dependently Typed, see Section 4 for the simply-typed case

Further reading on λ-calculus:

• Peter Selinger, Lecture Notes on the Lambda Calculus
• Ralph Loader, Notes on Simply Typed Lambda Calculus