§ Stuff I learnt in 2022

2022 was a weird year for me. I moved from India to Edinburgh to pursue my PhD, and a lot of the year was (and still is) getting used to what it even means to be a PhD student. Here's a run down of the things I learnt this year, and what the experience of doing this was.

§ Semantics of MLIR in Lean

The first project I took up was to define the semantics of MLIR , a new compiler infrastructure in the Lean4 proof assistant, titled boringly as opencompl/lean-mlir. While working on the project, I did a bunch of useful things:

§ Lean OSS work

I also began contributing to the proof assistant itself. In particular, I've been slowly chipping away at adding LLVM support , which got merged on the 31st, right before new years! The hardest part was learning a huge amount about low-level linkers, loaders, and other cross platform shenanigans. The sources I leaned against most were:
  • The CMake manual , which actually makes CMake sensible. I quite like CMake now, since I actually understand its semantics.
  • Linkers and Loaders , to learn a ton of the arcane details of how precisely loading works.
  • The GNU binutils , which were a lifesaver in debugging weird linker visibility issues.

§ Partial Evaluation

I was also interested in improving the performance of the code generator, and was frustrated that we in compilers kept rediscovering basic optimisation techniques over an over again. Partial Evaluation seemed like a powerful technique to prevent this waste, and I thus began reading the literature on partial evaluation. The best book I found was called Partial evaluation and automatic program generation , and I implemented the algorithms from the book . However, I haven't had the time to integrate these back into lean proper. Plans for next year!

§ Adjoint School And Category Theory

I wanted to learn more category theory, since I felt it was important as a type theorist in training to be fluent with category theory.
  • I was reading Categorical logic by Bart Jacobs, which describes how to reason about type theory using the machinery of fibered categories .
  • I attended Adjoint School , a summer school for applied category theorists, which was a blast. I learnt a lot from it, and read a bunch of papers from it!
  • I loved the paper Opinion Dynamics on Discourse Sheaves , which describes how to setup a 'discourse sheaf', a sheaf structure on a graph which models private versus public opinions. The punchline is that harmonic functions lead to 'harmonious' discourse amongst participants in the model!
  • Ohad pointed me to Probabilistic models via quasi borel spaces , which builds quasi-borel spaces, which is a closed cartesian category where one can interpret simply typed lambda calculus. This gives a nice denotational footing to probabilistic programming.
But to be honest, what I really took away from this was that I don't enjoy category theory as much as I enjoy geometry. Thus, I'm going to try to align next year such that I get to read more geometric concepts!

§ Logic

I wanted to learn logic and model theory, so I read George Boolos' book "Computability and Logic" . My two favourite theorems were:
  • The Compactness theorem , which points to the finiteness of the proof system we use, and how this impacts the logic itself.
  • The Lowenheim Skolem theorem, which shows that first order logic cannot control the size of its models.
I also wanted to learn what forcing was about, so I tried to read through the literature:
  • I began by reading Jech: Axiom of Choice , which was far too terse to grok, so I switched to reading the next lecture notes.
  • Independence of CH: an intuitive explanation was a readable account of the machinery of forcing! I wanted to get the account of forcing from the point of view of topi, for which I started reading the next book.
  • Sheaves in geometry and logic is a textbook on topos theory, which provide an account of forcing by building an object called a cohen topos . I didn't manage to get through enough of the book to really understand what the chapter on the cohen topos was doing, but I did get the vague idea. We seem to build a topos, and then use the internal logic of the topos to mimic the model we are building. The machinery of topos theory allows us to easily control the internal logic, thereby adding the axioms to ZF.

§ Frex

Ohad Kammar is a senior research fellow here at Edinburgh who I really enjoy talking to. He told me about a project he works on, frex, which stands for "free extensions". The TL;DR is that they wish to study how to write down simplifiers / computer algebra systems in a principled fashion. Their paper Partially static data as free extensions of algebras is a super readable account of their ideas. I quite enjoyed re-implementing the basic version in Haskell. I wish to implement their more recent, more complex dependently-typed version of the theory in Lean.

§ Ideas in type theory and proof assistants

Since I'm here at Edinburgh, I keep getting stray recommendations on things to read. A big shout-out to Andres Goens , Chris Hughes , Jesse Sigal , Justus Mathiessen , Leonardo De Moura , Li-yao Xia , Mario Carneiro , Ohad Kammar , and Sebastien Michelland for many of these pointers.
  • On Universes in Type Theory describes the difference between russel and tarski style universes.
  • Case trees are a data structure which are used in Coq and Idris to manage dependent pattern matching.
  • primitive recursors in Lean
  • congruence closure in intensional type theories describes how to extend the naive congruence closure algorithm in the presence of definitional equalities between types.
  • Difference between match+fix, as introduced by Theirrey Coquand in 'Pattern Matching with Dependent Types' , termination_by, and primitive recursion.
  • The idea of full abstraction, which asks the question of when operational and denotational semantics agree, first studied by Gordon Plotkin for PCF
  • Andrej Nauer's notes on realizability , which very cleanly describes the theory of realisability models, where one studies mathematical objects equipped with computational structure. this naturally segues into discussions of models of computation and so forth.
  • I am not a number, I am a free variable describes "locally nameless", a technique to manage names when implementing proof assistants.
  • Higher order unification is necessary when implementing the elaborator for a proof assistant. Unfortunately, the full problem is also undecidable
  • Luckily for us, Miller found a fragment called 'pattern unification' , where unification is indeed decidable. The key idea is to add a 'linearity' constraint which ensures that variables are not repeated into the pattern match, which makes even higher-order patterns decidable.
  • The Beluga Proof Assistant is a proof assistant whose logic allows one to reify contexts. This means that one can write shallow embeddings of programming languages, have all the nice power of the proof assistant, while still reasoning about binders! I found the way in which Beluga makes such invasive changes to the metatheory in order to allow reasoning about binders to be very enlightening.
  • The HOL light proof assistant and Isabelle/HOL are both based on higher order logic, and alternate, untyped foundations for proof assistants. I feel it's important for me to know the various ideas folks have tried in building proof assistants, and I was glad to have been pointed to Isabelle and HOL. I want to spend some time this year (2023) to learn Isabelle and HOL well enough that I can prove something like strong normalization of STLC in them.
  • Fitch style modal logics are a systematic way to build type theories with modalities in them. These are typically used to create type theories that can reason about resources, such as concurrent access or security properties. The paper provides a unified account of how to build such type theories, and how to prove the usual slew of results about them.
  • Minimal implementation of separation logic: Separation Logic for Sequential Programs explains how to write a small separation logic framework embedded in a dependently typed progrmaming language. I translated the original from Coq to Lean , and the whole thing clocks in at around 2000 LoC, which is not too shabby to bootstrap a full 21st century theory of reasoning about parallelism!
  • Telescopic Mappings in Typed Lambda Calculus builds the theory of telescopes, which is the basic notation that's used when describing binders in dependent type theory. I had no idea that this had to be developed; I shudder to think how ugly notation was before this paper! I can't help but feel that this paper did for dependent type theory what einstein summation convention did for tensor calculus: provide compact notation for the uninteresting bits to allow us to to talk about the interesting bits well.
  • When talking to Leonardo, I learnt that the hardest part of implementing a homotopical theorem prover was the elaboration of pattern matching. Pattern matching without K explains how to do this, and also made clear for me at what step UIP is used during pattern matching --- when refining on indexes of a type.
  • The garden of forking paths to reason about lazy programs describes how to use Clairvoyant call by value to reason about laziness in a convenient fashion.

§ Computational group theory

I was confused about what I should pick for my PhD topic, and I briefly flirted with the idea of working on computational group theory. I genuinely loved a bunch of the papers in this space, but alas, I couldn't see myself seriously working on these, due to the lack of a clear and focused problem that I coulf work on. I did read some cool papers regardless:

§ Automated theorem proving

I wound up reading a little on how to implement automated theorem provers (SAT/SMT solvers). This space is huge, and I only got a cursory glance at it from the Decision procedures book . Even so, it was neat to learn the core ideas:

§ Common Lisp

I got turned off of writing scripts in Python because writing parallel processing is a pain, so I did the obvious thing: picked up common lisp!
  • I mostly learnt lisp by reading practical common lisp and hanging out on ##lisp on libera IRC.
  • I absolutely loved the REPL driven development enabled by emacs+ slime, and this has definitely set a gold standard for how programming language interaction ought to feel like.
  • I was floored by some of the comon lisp projects I saw, such as cepl , the code-eval-play loop for rapid shader development! His videos are super cool , and I highly recommend them to anyone who wants to get a flavour of LISP.
  • I'd like to work through Let over Lambda , a book that explains all sorts of macro shenanigans!

§ Non fiction and fiction

I wound up reading a bunch of sci-fi this year, since I wanted to work my way through the Nebula award winners. My favourites were:
  • All Clear by Connie Willis paints a great picture of the blitz during WW2. It feels surreal to have visited london and edinburgh and glasgow and all the other places that are name dropped in the book, it felt visceral.
  • The Annihilation series ), which has the creepiest vibes in a book I've ever read.
  • Accelerando , which had a really neat take on a resolution of the Fermi Paradox, and just an overall fun tone.
  • The book of all skies by Greg egan, which as usual explores a neat universe, this time with some kind of monodromy.
  • Honorary mention to Perfect State by Brandon Sanderson , a cute novella with a really neat twist at the end I didn't see coming.
As usual, I was reading some more sciencey things, this time on chemistry and nanotechnology, which were the books Ignition! An informal history of rocket liquid propellants , Inventing Temperature , and Engines of creation .

§ Looking Back

When I started writing this blog post, I felt that I hadn't learnt as much as I did in 2019 . However, I now see that I've learnt a bunch of things, just in a small domain (proof assistants / type theory / logic). To be honest, this makes me kind of sad; I miss learning different things, and I feel like I haven't gotten closer towards some of my life goals of things I want to learn --- the standard model of particle physics, the proof of resolution of singularities, and other such goals. I'm going to try to make sure 2023 is more diverse in what I read, to make sure I'm happy and sane, while continuing to become an expert in proof assistants :). With that said, I'd like to set concrete goals for 2023:
  • Learn enough QFT to know what the hell renormalization is.
  • Learn enough QED to be able to explain what a feynmann path integral is.
  • Get good enough at juggling to be able to juggle three balls consistenty.
  • Write my own proof kernel for Lean.
  • Implement and write the paper about elaboration of mutual inductives for Lean, and start thinking about coinductives.
  • Continue working on Lean's LLVM backend, and make Lean the fastest functional programming language in the block.
  • Learn to cook a proper three course meal consistently.
  • Get good enough at djembe to play kuku consistently.
  • Get good enough at the guitar to strum Snow and Can't Stop well enough.
  • Build a routine for shuffle dancing, so that I can dance consistently to a song.
  • Learn to rock climb well enough that I can do V4's consistently.
That looks like an ambitious list, and I'm glad it is. I'd like my years to be full of interesting challenges and neat things I can point to at the end of year! With that said, happy new year!