Part II / Part III Project Suggestions

A category-theory inspired compiler

TLDR: Implement the compiler from Using functor categories to generate intermediate code in a dependently-typed language of your choice. You don’t need to know anything about dependent types or category theory beforehand!

Simply-typed lambda calculus has semantics in cartesion closed categories, and presheaf categories $Set^{C^{op}}$ are cartesion closed. A presheaf $P \in Set^{C^{op}}$ can be considered as a family of sets $\{P_c\}_{c \in C}$ varying over a category of states $C$ – it could be the states of memory locations, so that we can interpret lambda calculus with stores as semantic objects varying over the states of stores. For our purpose, we’ll borrow John Reynold’s idea, taking $C$ a category of compiler states, and interpret lambda calculus programs as the intermediate code generated at some state. That’s a cat-theory inspired compiler!

As Reynold remarks, dependent types are required to define presheaf actions but he couldn’t do this in the 90s
– there were no dependently typed programming languages around! Now, we have well-developed tools like Agda, Coq, Idris2, etc., and we can finally implement Reynold’s idea.

We can start with a cat-theory-based interpreter for simply typed lambda calculus, then extend it with the imperative features mentioned in Reynold’s paper: stores, subroutines, and iterations. Possible extensions include:

• Adding optimization stages
• Adding exception handling
• Writing mechanized proofs for correctness properties of the compiler-generated code

Supervisions

• Denotational Semantics, since 2023
• Compiler Construction, since 2024
• Optimizing Compilers, since 2023
• Concepts in Programming Languages, since 2023