Adventures in Type Theory 4 — The Ship of Thesis

Published: 2025-10-01

Part of the Adventures in Type Theory series

Location: FS04, William Gates Building (52.210434, 0.091859)

Time: 2025-09-30T14:00+1

It’s been a long journey!

The type theory starts after the Prelude section.

Prelude

Location: Darwin College (52.20035, 0.11422)

We set sail from Termini Imerese to the island of Vulcano¹. Well, we sailed part of the way, but after making the mistake of letting me at the wheel, we had to switch to the engine…

Anyways. From there, we move on to the island of Lipari, where we part ways, with the rest of the crew going to Stromboli. It was time to get somewhere with better Internet.

I took the ferry back to Messina, and from there, the train back to Termini Imerese. On the long march to the train station, I think locally nameless thoughts. It was time for another attempt at the covalence theorem prover, as the end of my PhD loomed. So I try formalizing the new type theory, this time with cumulative universes and a new approach fusing locally-nameless style with the indexed term types of logrel-mltt. At the same time, much meditation on SSA occurred.

I arrive at Termini Imerese and ride my bike back to Messina, where I stay at the wonderful La Badia Bed and Room. I arrive at 1 AM, much later than planned, as I got lost on the way and had to find gas. Thankfully, the owner finds me at the door and, though I don’t have cash, allows me to stay, with a promise to go find an ATM the next morning and pay.

The owner is a jovial psychiatrist who helps youth with addiction issues, and offers me numerous coffees. I, of course, accept these, and then head out into the city to find cash and breakfast. Tempted by the seafood available at the local supermarket, I decide to stay another night.

I leave the next day, having laid down the bones for what I’m calling Gödel-Tarski Type Theory, or GT3, and make for Balzano in Calabria, where my mother’s mother’s family lives. There, I receive free food, free board, and poor, but better than shipboard, Internet. And I also encounter the lowest density of English speakers I’ve seen in my life, so far. Almost everyone speaks only Italian.

This provided the perfect environment to get some work done. A little thesis, and a lot of theorem proving later, and GT3 is taking shape and nearly ready for implementation. I take the time to plan out my next steps in general. But all good things come to an end, and eventually, it is time to head northwards, and back to work. To make sure I actually get there on time, I book some sushi with a good friend of mine in London at 2025-09-19T18:00+1. A precise arrival date does wonders for trip planning.

I make for Rome, where, carrying what I thought was most of GT3. I get distracted at the gas station, and the night deepens, so, at 1:30 AM or so, I decide to stop at the neighboring city of Aquina. As a first shot, I make for La Vecchia Quercia, but I’m too late. Most of the places I call are closed, or expensive, and at this point, being 2:30 AM, I’d be buying just a few hours of quality sleep.

So I decide to do some science and just sleep in the field. It’s warm, right.

Verdict: uncomfortable, due to rocks, and the occasional chill. But very doable in Italian summer weather.

Up, and onwards. My charger is broken, so I need to get a new one. Charging up my navigator before that in the city, we continue down to Rome, where I plan to meet a friend from Cambridge who’s passing through for a conference. It’s a confusing place: all roads lead there, so once you get there, the roads just lead to themselves, and you’re completely free. It’s a sad day, when you understand the quote

Freedom is an ocean. You can drown in it.

But there is no victory without sacrifice. It is only through that sadness, that the happiness of self-actualization, of true freedom, can be reached.

That’s what I keep telling myself about graduation, anyways.

I stay at the powerfully-named Happy Village e Camping Roma. After a day of food, sightseeing, and formalization (I realized that I forgot to add the natural numbers to GT3…), it’s time to bounce.

I make for Milan, but once again I fall prey to the temptations of the gas station. So I take a detour to Bologna, where I hope to meet Vikraman, which is always an excellent experience. Alas, he has left for the UK the previous day. Such is fate!

Armed with only his list of recommendations, I translate into the mountains near Bologna, through freezing mists, and arrive at the B&B Nina at 3 AM. The host is exceedingly hospitable, and, spared from roughing it in the mountains, I fall deep into hypersleep, gathering strength to face the morrow.

I spend a quiet day working on GT3 and tapping here and there at some locally-nameless SSA ideas. Night falls once more, and the clock is ticking to return to Cambridge. So I make for Milan once more, stopping at a local restaurant on the way. And, almost a month later, I find myself once more at the Idea Hotel Milano San Siro.

The sun rises, and I burn rubber on the road to Switzerland. Elas! At the very final gas station between Italy and Switzerland, I am once more waylaid by that ever crafty opponent, myself! Ah, the ruses of the French!

A good friend from Toronto and I spend the day there on the phone, discussing covalence, mathematical superintelligence (I am very excited about Harmonic… we need to integrate Aristotle with covalence, or something…), game theory, and other fun topics.

But then it is 9 PM and the Alps await. And I do not want to bankrupt myself finding a hotel in Switzerland.

I was so excited to see the Alps in the day. It will have to wait till next time, elas. Through the inky dark, a point of light flies.

Adventures ensue. I get held up in front of a closed tunnel, and my clutch starts acting up again (but, thankfully, the bike still works). And so it is nearly 4 AM when, exhausted, I find myself back in Mulhouse, at the B&B I had originally booked before the drain plug incident.

The morning comes once more, and I meet with Neel. He’s excited about covalence, and we discuss thesis plans. I get some Indian food and ride on over back to Seedz Motorsport to discuss clutch and refunds. They couldn’t find anything wrong with the clutch (which was strange: I definitely noticed it slipping, but just at high RPM, usually on a hill; even lugging it at low RPM was/is fine), but agreed to send over a refund due to the drain plug incident.

It was weird to be back in Woustviller after all this time. Well, not much time, but it felt like an aeon. Much thinking has been done. I went back to the Kebab Le Bosphore, and finished hammering out support for the natural numbers. As the last axioms for GT3 fell into place, it was closing time, and time for me to ride to Calais, lest I miss sushi. So we hit the road.

Gas stations are dangerous. It seems that the closer I go to where I was forged, the more powerful I become. Once more, I find myself waylaid by my dastardly foe. At 3 AM, I decide just to sleep there. Attendant was a cool guy. Lots of food, warm, and open all night. Like a little mall.

It’s 6 AM, I’m up, I get some food, and we have precisely 12 hours to be ready for London.

We ride for Calais! For the first time since I began this journey, I crack a monster: “Top Speed,” the French version of Lewis Hamilton flavor. Already, we’re coming home.

The ride home is not uneventful. But I make it to the train, with some time to spare, and take an early instance of Le Shuttle. Through the tunnel, and it’s an easy ride to London, back on the wrong side of the road. There’s a dress code, but I have just enough time to shower and go buy a shirt from Marks & Spencer. I’m on three hours of sleep, but I’ve survived worse.

I have a good time, enjoying the last brief period of rest before the excellently-named HOPE, followed by the Thesis March.

The morning comes, we have a nice late breakfast of chicken at Pitted Olive. And then I ride back to Cambridge.

Ten mostly uneventful days followed, as I sorted various things out and got back on track for thesis, teaching, et al.

It is 2025-09-29T10:48+1. A long time ago, my father remarked that the garden behind Darwin was about as close a representation of Eden as one could get on Earth. I’ve warmed to this sentiment.

So I’m standing under the Tree of Knowledge of Good and Evil, a year and a month, or a year, later, and, I reflect that, as Steve Jobs might say, it’s time to become a real artist, and ship.

Inductive SSA

Location: FS04, William Gates Building (52.210434, 0.091859)

Time: 2025-10-01T23:03+1

As I was just saying, a while back, I wrote an article on building an inductive representation of SSA, which later became the core of my TOPLAS submission, The Denotational Semantics of SSA, which must now become the core of my thesis. It’s time to work on shipping that.

Recall that a program written in 3-address code consists of a control-flow graph $G$ made up of basic blocks $β$. Each basic block is a straight-line sequence of instructions (often of the form $x = \mathsf{op}(y, z)$, hence the name three-address code) followed by a single terminator instruction, which can jump to other basic blocks. Examples of terminators might be an unconditional jump to a label $ℓ$, or a conditional branch (if-then-else). By convention, we’ll assume $G$ has a distinguished entry block without a label.

So, to compute 10!, we might write the C program

let n = 10;
let mut i = 1;
let mut a = 1;
while i < 10 {
    a *= (i + 1);
    i += 1;
}

We could compile this to three-address code to get

    n = 10;
    i = 1;
    a = 1;
    goto loop;
loop:
    if (i < n) { goto body }
    else { return a };
body:
    t = i + 1;
    a = a * t;
    i = i + 1;
    goto loop

Which blocks can syntactically jump to each other form the (directed) edges in the CFG. So for example, this CFG has edges

ENTR -> loop
loop -> body
loop -> EXIT
body -> loop

We might make this into a formal grammar as follows:

// Instructions
//
// We allow a variable as an instruction for renaming
o ::= op x₁ ... xₙ | x
// Basic blocks
β ::= x₁,...,xₙ = o; β | τ
// Terminators
τ ::= goto ℓ | if o { τ₁ } else { τ₂ } | return o
// Control-flow graphs
//
// Note: the entry block is first
G ::= β | G ; ℓ : β

Note constants $c$ are just nullary operations op; we allow the if-statements in terminators to be nested for simplicity, and also because that can be used to emulate a switch.

One question the astute reader may ask is what the scoping rules for variables are: while we might just raise an error on using an undefined variable (or declare this undefined behavior, more likely), we’d like to have a static analysis which guarantees that all variables are defined before use.

In graph theory, a node $n$ in a directed graph with a distinguished entry node $e$ is dominated by a set of nodes $D$ if every path from $e$ to $n$ passes through an element of $D$. We’ll say $D$ strictly dominates $n$ if $D \setminus \{n\}$ dominates $n$.⁵

We say a single node $d$ (strictly) dominates $n$ if $\{d\}$ (strictly) dominates $n$, in particular, $d$ strictly dominates $n$ if and only if $d$ dominates $n$ and $d ≠ n$.

Letting $D_x$ be the set of basic blocks containing a definition of $x$, we know that a use of $x$ in block $β$ with label $ℓ$ is well-scoped if

• $ℓ ∈ D_x$ and the usage of $x$ is after the first definition of $x$ in $β$
• $D_x$ strictly dominates $ℓ$, since all paths to get to $ℓ$ have already defined $x$

We want to restrict our attention to such well-scoped programs, since we can give them a semantics even in settings without a clear notion of an error, and in particular, we can give them a categorical semantics.

There are three regularizing tweaks we might want to make as type theorists:

• Introduce nullary tuples $()$ and binary tuples $(v, v')$ of values, and make operations take a single tuple $v$, likeso:

  // Tuples
  v ::= x | (v₁, v₂) | ()
  // Instructions
  o ::= op v

  An $n$-ary tuple can then be implemented as just $(x_1, (x_2, (x_3, ...)))$ (or we can associate on the left, of course). Then we can regularize our let-bindings as

  // Basic blocks
  β ::= x = o; β | (x, y) = o; β | τ

  which of course we can use to desugar any pattern destructure $v = o; β$ in the obvious manner. This avoids tedious work with $n$-ary shifts to our de-Bruijn indices when using those, since adding one and two has much better defeqs.

  We do do this in both our SSA papers². We’re not quite going to do this here, yet. But keep it in mind.

• Replace return with a branch to a distinguished exit label; with return now just syntax sugar.

• Replace if-then-else with case-statements case (o) { ι₁ x₁ : τ₁ ; ι₂ x₂ : τ₂ } (if-then-else just desugars to an anonymous case split on $1 + 1$).

  Well, our paper does binary case-statements, but this in fact leads to suffering later when we want to prove things like completeness and Böhm-Jacopini, so we’ll learn from that and do an $n$-ary statement. Because I am unfathomably lazy and want to use my C syntax highlighter, we’ll keep the keyword switch³, and so write switch (o) { ι₁ x₁ : τ₁ ; ... ; ιₙ xₙ : τₙ }.

  In the paper, injections become part of the grammar for instructions $o$. Here, we’re going to be lazy and say injections become part of op; nullary injections (we’ll write these $ιₙ\;()$ for disambiguation) for components of unit type, and unary in general. We might need to tag them with types, or something. We’re being lazy here because we have a different goal in this section than in the paper.

We’ll do the latter two only. So terminators become

// Terminators
τ ::= goto ℓ | switch (o) { ι₁ x₁ : τ₁ ; ... ; ιₙ xₙ : τₙ }

Now, SSA can be viewed as a property of a 3-address program: every variable name $x$ having precisely one definition; i.e. static single assignment⁴. If a 3-address program has no variables whose value is (syntactically) control-flow dependent, we can re-name variables (essentially, appending a time-stamp) to convert it to an equivalent program in SSA; e.g.

    x = y + z;
    x = x + 3;
    if (x > 3) { return 5 } else { goto rest };
rest:
    x = 3 + y;
    return x;

becomes

    x₀ = y + z;
    x₁ = x₀ + 3;
    if (x₁ > 3) { return 5 } else { goto rest };
rest:
    x₂ = 3 + y;
    return x₂

The idea is we’re just numbering each syntactic re-definition of $x$, and then replacing each use with the specific definition it is referring to, where “John” is replaced with “John Smith” or “John Doe” based on context. But not every program is unambiguous with respect to control-flow:

    if (φ) { goto left } else { goto right };
left:
    x = 3;
    goto then;
right:
    x = 5;
    goto then;
then:
    return x;

If $x₀ = 3$ and $x₁ = 5$, which $x$ are we returning? Standard SSA solves this by introducing special $ϕ$-instructions or $ϕ$-nodes which take a different value depending on where we just came from in the CFG. So for example, since if we came from left we’d use $x₁$, but use $x₂$ if we came from right, we could introduce a $ϕ$-instruction representing this as follows:

    if (φ) { goto left } else { goto right };
left:
    x₀ = 3;
    goto then;
right:
    x₁ = 5;
    goto then;
then:
    x₂ = ϕ { left : x₀ ; right : x₁ }
    return x;

Often, we allow pure operations, or at least constants, in $ϕ$-instructions, so we could even simplify this to

if (φ) { goto left } else { goto right };
left:
    goto then;
right:
    goto then;
then:
    x₂ = ϕ { left : 3 ; right : 5 }
    return x;

These have slightly unintuitive scoping rules: we can add a label $ℓ : o$ to a $ϕ$-instruction if $o$ would be well-scoped at the end of the basic-block $β$ labelled $ℓ$⁶. We’ll maintain the invariant that $ϕ$-instructions cannot access other variables in their own block (so the scope is precisely that at the end of $β$, rather than the union of the instructions before the $ϕ$-instruction and those visible at the end of $β$); since $ϕ$-instructions are pure, we can also easily maintain the invariant that $ϕ$-instructions are always before any non-$ϕ$ instruction in their basic block by simply floating them up to the top⁷.

Thankfully, by a mechanical transformation, we can show that $ϕ$-instructions are precisely equivalent to simply, for each $ϕ$-instruction $x_1,...,x_n$ at the front of a basic block $β$, adding parameters $x_1,...,x_n$ to the label $ℓ$. Then any jump to $ℓ$ needs to provide values for each parameter $x_i$, which correspond precisely to the value in the $ℓ$-branch of the $ϕ$-instruction originally defining $x_i$. This, hopefully, makes the scoping rules for $ϕ$-instructions obvious: it’s just the regular scope at where the values are actually computed (namely, just before branching to $ℓ$).

In terms of formal grammar, we get

// Instructions
//
// We allow a variable as an instruction for renaming
o ::= op x₁ ... xₙ | x
// Basic blocks
β ::= let x₁,...,xₙ = o; β | τ
// Terminators
τ ::= goto ℓ(o₁,...,oₙ) | switch (o) { ι₁ x₁ : τ₁ ; ... ; ιₙ xₙ : τₙ }
// Control-flow graphs
//
// Note: the entry block is first
G ::= β | G ; ℓ(x₁,...,xₙ) : β

The above program then becomes

    if (φ) { goto left } else { goto right };
left:
    x₀ = 3;
    goto then(x₀);
right:
    x₁ = 5;
    goto then(x₁);
then(x₂):
    return x;

while our factorial program becomes

    n = 10;
    i₀ = 1;
    a₀ = 1;
    goto loop(i₀, a₀);
loop(i₁, a₁):
    if (i₁ < n) { goto body }
    else { return a₁ };
body:
    t = i₁ + 1;
    a₂ = a₁ * t;
    i₂ = i₁ + 1;
    goto loop(i₂, a₂)

These hopefully have much more obvious semantics: tail-calls. Indeed, since every variable has a unique definition, it’s like we’re using a let-binding rather than a mutable variable. We really want things to be “as-functional-as-possible,” since that makes building a nice compositional semantics a lot easier. But we still don’t know hour our let-bindings are scoped. And induction on CFGs by doing induction on the list of basic blocks is… suboptimal…

What we want to do is figure out how to switch to lexical scoping, in a way which gives us a good induction principle on SSA programs.

Since every variable $x$ has a unique definition point $d$, dominance-based scoping in SSA simplifies to requiring that every usage of $x$ is strictly dominated by $d$; i.e., in a basic block strictly dominated by $d$ or in the same basic block as $d$ and located after it. Thankfully, we note that the dominance relation is more than just a partial order on reachable blocks (in general it is a preorder), it’s actually a tree.

In particular, consider a directed graph with distinguished entry point $(G, e)$ again. We’ll say a node $n$ has immediate dominator $d$ if:

• $d$ strictly dominates $n$
• $d$ does not strictly dominate any other node that strictly dominates $n$

It turns out that every node reachable from $e$ except $e$ itself has exactly one immediate dominator, forming the dominator tree, and moreover that the dominance relation on these nodes is just the reflexive transitive closure of the immediate dominance relation.

Anyways, long story short, it turns out that lexical scoping w.r.t. the dominator tree is exactly the same as dominance-based scoping. So if we just encode the dominator tree syntactically, we don’t need to bother with dominance-based scoping.

So how do we do that?

We borrow some ideas from MLIR and introduce the concept of a single-entry-multiple-exit region, which for us is just a subtree of the dominator tree. We want to nest up our graph in such a way that the nesting structure is the dominator tree (or rather, is compatible with the dominator tree: if $β$ is nested within $β'$, then $β$ must be dominated by $β'$, but we can have $β$ dominated by $β'$ without the nesting so long as $β$ does not use any variables in $β'$).

So more specifically, instead of treating our program as a CFG-with-entry-block $G$, we instead treat our program as a region $r$, thought of as a subtree of the dominator tree, with the root being the entry block. This region consists of a basic block and a collection of children, which are only visible to each other and to the root. This enforces dominance, since the only way to get to the children is through the root; ergo, the root dominates the children.

As a grammar, it is natural to replace the syntactic category of basic blocks $β$ with the category of regions $r$, as follows:

// Instructions
//
// We allow a variable as an instruction for renaming
o ::= op x₁ ... xₙ | x
// Regions
r ::= x₁,...,xₙ = o; r | τ where { L }
// Terminators
τ ::= goto ℓ(o₁,...,oₙ) | switch (o) { ι₁ x₁ : τ₁ ; ... ; ιₙ xₙ : τₙ }
// Children
L ::= · | L ; ℓ(x₁,...,xₙ) : r

Note that $r$ recognizes the same strings as β where { L }, and indeed, collecting all the instructions in a region into an array, the data in a region is basically a basic-block with children:

struct Region {
    instructions: Vec<Instruction>,
    terminator: Terminator,
    children: Map<Label, Region>
}

But for induction, x₁,...,xₙ = o; r | τ where { L } gives a nicer induction principle, and more importantly, it’s easier to give it typing rules. The two data types are trivially isomorphic though!

Now, for the typing rules a data structure like this would have, perhaps a peek at The Denotational Semantics of SSA is in order. But I need to re-work all that to be locally-nameless, which we should do in a future post.

But specifically, I’d like to actually represent general MLIR SSACFG regions. And those:

• Allow instructions to take regions as parameters
• Use instructions as terminators (in the typing rules we need to check they are valid terminators). We’ll just pass in regions $r₁,...,rₙ$, and let the user handle labels in the production tm.

Syntactically that’s not too complex:

// Instructions
//
// We allow a variable as an instruction for renaming
o ::= op x₁ ... xₙ r₁ ... rₙ | x
// Regions
r ::= x₁,...,xₙ = o; r | τ where { L }
// Terminators
τ ::= tm r₁ ... rₙ
// Children
L ::= · | L ; ℓ(x₁,...,xₙ) : r

In fact, a first pass at graph regions might look like

// Instructions
//
// We allow a variable as an instruction for renaming
o ::= op x₁ ... xₙ r₁ ... rₙ | x
// Regions
r ::= x₁,...,xₙ = o; r | τ where { L } | τ graph { O }
// Terminators
τ ::= tm r₁ ... rₙ
// Children
L ::= · | L ; ℓ(x₁,...,xₙ) : r
// Mutually recursive definition graph
O ::= · | O ; x₁,...,xₙ := o

But this exposes some irritating discrepancies with MLIR (though the first might be useful):

• Graph regions can be preceded by let-bindings, which enforce a DAG on the operations in them
  • A “daggy” graph region is a useful thing to have though, by requiring $O$ to be empty… a dialect can require that!
• Graph regions can appear as children of non-graph regions in a where-block, which is… weird…
• Graph regions with a single block can opt out of having a terminator

Let’s take that

// Instructions
//
// We allow a variable as an instruction for renaming
o ::= op x₁ ... xₙ r₁ ... rₙ | x
// Regions
r ::= s | g
// SSACFG regions
s ::= x₁,...,xₙ = o; s | τ where { L }
// Graph regions
g ::= τ? graph { O }
// Terminators
τ ::= tm r₁ ... rₙ
// Children
L ::= · | L ; ℓ(x₁,...,xₙ) : r
// Mutually recursive definition graph
O ::= · | O ; x₁,...,xₙ := o

It’s a good start. But we need to think long and hard about how to make this nice and locally nameless, give it dialect-friendly typing rules, and eventually, a good categorical semantics.

I plan to start with SSACFG, for simplicity. One thing at a time. Graph regions on their own can also be interesting. But, that’s for later articles.

Toodles!