Presheaf lectures

Category theory recap

We treated categories, functors, natural transformations, and maybe also monads and monoids.

Bartosz Milewski has a blog on category theory that people are enthousiastic about. The relevant sections would be:

Another place where you can learn about monads, is in the Haskell tutorial Learn you a Haskell for great good, chapter A fistful of monads.

Presheaf lecture 1 (Nov 4, 2022)

What is an algebraic/type theory, and what is a model?

Main idea: we can specify a unisorted or multisorted algebraic theory or programming language by

The framework of algebraic theories then tells us automatically what it means to give a model of that theory/language.

In the lecture I used slides 6 and 7 from my recent TyDe-presentation, for which there is also a video.

Relevant resources:

STLC as a multisorted algebraic theory (MAT)

See def. 8.1 of my KEML-note, although it's a bit brief.

Types can be regarded as single-variable contexts, so terms can be regarded as substitutions.

A model is then a category whose objects are syntactic contexts (but with an unimportant trick we can model syntactic contexts by different, semantic contexts) and whose morphisms are semantic substitutions.

To model the empty context (and possibly a unit type), we need a terminal object. To model context extension (and possibly pair types) we need cartesian products. So the category needs to be cartesian, which means that it has a terminal object and binary cartesian products.

To model function types, lambda-abstraction and application with beta- and eta-rules, the model needs to be cartesian closed.

In short, models of the STLC are exactly cartesian closed categories (CCCs).

Set model of the simply-typed lambda-calculus (STLC)

I don't really have a good resource here.

Presheaf lecture 2 (Nov 25, 2022)

Guarded type theory

Some resources about the type system itself are:

Single-clock guarded type theory can be modelled in the topos of trees, i.e. the category of presheaves over ω.

I explained the model of the guarded STLC in Psh(ω), which I don't have a good reference for but I will come back to it in the dependent case.

Parametricity

  1. Motivation

    • The book "Types and Programming Languages" (a.k.a. TAPL) by Benjamin C. Pierce, chapters 23 and 24 and prerequisites (see the dependency graph in the book's front matter). This book is also the lecture material of the Formal Systems course.
    • An accessible paper about parametricity: Wadler, 1989, Theorems for Free
  2. Reflexive graphs are presheaves:

    See e.g. my PhD, example 2.3.8.

Presheaf lecture 3 (Dec 2, 2022)

  1. Parametricity of System F(ω); Reynolds' relational model for System F and how you need reflexive graphs if you want to generalize to Fω.

  2. Parametricity is only interesting when we look at languages with type variables (so not the STLC, but System F(ω) or dependent types). I've noted that these are not multisorted algebraic theories (MATs) but generalized algebraic theories (GATs, the dependent generalization). I haven't defined what a GAT is, but just like for MATs, if we specify a GAT then that automatically tells us what a model of that GAT looks like. For System F(ω) and dependent types, the "infrastructural" part of such a model is a category with families (CwF). I would suggest section 3.2.1-2 of my phd thesis (and all of chapter 3 for the curious), or the sources cited there.

  3. I've started sketching how presheaf categories constitute a CwF, and I think I was in the process of explaining what a type is in a presheaf model when the lecture ended. This would correspond to sections 4.1.1-2 of my PhD thesis (or the sources cited there). Examples 4.1.1-3 are exactly about sets, reflexive graphs, and step-indexed sets, so they are exactly the examples from the lecture.

Presheaf lecture 4 (Dec 16, 2022)

  1. Presheaf categories are Categories with families (CwFs)

    • What is a type in a presheaf category (via slices & local democracy)
    • What is a term in a presheaf category (via sections of slices)
    • Boring type formers
    • Pair and Σ-types

    Relevant resources: See below.

Further reading

  1. Presheaf categories are Categories with families (CwFs)

    • Function and Π-types

    Relevant resources:

  2. Recap: how does the parametric model pay off?

  3. the Yoneda-embedding & Yoneda-lemma

    See sections 2.3.1-4 of my PhD

    • Function and Π-types again
  4. Other applications: homotopy/directed/nominal/multiclock type theory

    • Perhaps sketching the base categories
    • Products of base categories

Advanced/optional: