Geb Reading Group Syllabus
Purpose
This document is intended to summarize the background, especially in category theory and polynomial functors, required to understand how Geb works. It will serve as a guide to topics for the weekly reading group, and for attendees on how to prepare.
Practically none of the following is required just to write code in Geb! But it is required to understand how the language works under the hood, and that would also enable a programmer to use more of it.
Learning outline
The two main threads of theory underlying Geb are category theory and polynomial functors. To some degree I am treating the former as the theory of (programming) languages and the latter as the theory of data structures, but in Geb they are intertwined, defined through mutual recursion: category theory defined by data structures, data structures given semantics by category theory, and â€ś(programming) languageâ€ť emerging as a notion of its own (broader than â€ścategoryâ€ť).
The big picture
The end goal of the language definition of Geb â€“ the point at which the language itself is finished and all else is libraries â€“ is what I have been calling â€śprogramming languages Ă la carteâ€ť. That is a reference, to â€śData Types Ă la Carteâ€ť, so the founding paper there (see the Bibliography) is one place you might start. It illustrates how to define data structures in ways which allow for more combinators than traditional explicitlyrecursive ADTs. Geb aims to extend this notion to programming languages â€“ defining them in terms of individual language features and combinators on languages themselves.
That possibility emerges from founding category theory itself on polynomials.
Track: category theory
Fortunately, but not just coincidentally, the aspects of category theory underpinning Geb are mainly the foundational ones â€“ the first few that are typically presented in books on category theory. One of my aims in the reading group will be to communicate these foundations in terms that will be most familiar to programmers â€“ each of them has a clear analogue in and application to programming.
Here is a rough order of topics Iâ€™d recommend.
Definition

The axioms which define a category

The notion of isomorphism

Question: what aspects of programming languages could be expressed as categories?
The category of categories

Functors

Natural transformations

Question: which programming language constructs could be viewed as functors? As natural transformations?
Slice categories and (co)presheaves
Slice categories are the standard way of expressing dependent types in category theory, so they are particularly relevant to programming with formal verification. They are also a step on the way to understanding the more general notion of (co)presheaf.
Adjunctions, universal properties, representable functors, and the Yoneda lemma
Riehl is a superb reference on these intertwined topics, but also quite dense. They are perhaps best learned by example, of which several follow below. Geb turns their use somewhat on its head: instead of defining â€śuniversal propertyâ€ť in terms of categories, Geb defines polynomials without explicit reference to (although with antipication of) category theory, then universal properties in terms of polynomials, then categories in terms of universal properties. This sequence allows the intermediate definition of â€śprogramming languageâ€ť in terms of universal properties, distinct from, though closely related to, that of â€ścategoryâ€ť.
Examples of universal properties
The following examples should help to absorb the notion of â€śuniversal propertyâ€ť itself, but are also precisely the ones which underlie Geb, and programming languages in general. As such, they also underlie category theory itself â€“ they are the ones in terms of which category theory can be homoiconic (can write itself).
For each of these examples, therefore, the question is: what programming language concept(s) do these universal properties correspond to?

Terminal objects

Initial objects

Products

Coproducts

Homobjects (exponentials)

Initial algebras

Terminal coalgebras

Free monads

Cofree comonads

Equalizers

Coequalizers

Pullbacks

Pushouts

Limits

Colimits

Ends

Coends

Kan extensions
Track: polynomial functors
By far the most comprehensive, uptodate reference that I know of on this topic is from the Topos Institute â€“ a book which is still being updated at least as of the last few months, and an accompanying video series (with more relevant videos frequently produced). The book was originally called Polynomial Functors: A General Theory of Interaction; â€śGeneralâ€ť has since been changed to â€śMathematicalâ€ť. The bookâ€™s website is in the Bibliography.
The book is large and contains many examples and applications; many of the formulas and theorems have been coded in Gebâ€™s Idris implementation, and in many cases Iâ€™ve ported them to the dependentlytyped context (that is, polynomial functors on slice categories). The most important thing to take from it is that there are many ways of viewing polynomial functors â€“ if you can understand each and how to translate among them, then you will understand how to use them to write data structures, programming languages, category theory, and Geb in particular.