Weeknote 2026 W7

Adding equality

Before I came to Glasgow, my elaborator did not have any kind of equality type. I wanted to do observational equality types because there is a good treatment of quotient types in observational equality types.

Talking with Bob really helped me understand what makes observational type theory tick. In particular, observational type theory very carefully avoids ever looking at the proofs of equality types. It is surprisingly subtle how to recover normalization and canonicity in this setting, and it wasn’t until Bob was looking over my shoulder as I wrote the evaluator that some of the smaller details actually made sense to me.

I am worried about how observational equality will interact with unification. I had an idea on the train on Wednesday, which was to weaken proof irrelevance (which conflicts with unification) to saying that the equality type between two proofs of a proposition was a definitional singleton.

However, if I’m going to do this in OTT, I have to actually do a lot more computation with proofs of equalities than is typically done. Anyways, it’s an interesting design space. I still have to understand unification better.

Identifying which theories should support free models

In my type theory, if I have

theory Graph := sig
  V : Query
  E : V -> V -> Query
end

theory Paths (G : Graph) := sig
  open G
  P : V -> V -> Query
  refl : (v : V) -> P v v
  snoc : (a b c : V) -> P a b -> E b c -> E a c
end

then for any G : Graph, I should be able to ask for the free model of Paths G. However, it is not true that I should be able to ask for the free model of G.V. The difference is that Paths G only postulates elements of types that it also postulates. Bob had the idea of handling this with a modality, which “locked away” all previous types and prevented them from showing up in the codomain of a term constructor. However, we couldn’t figure out what the semantics for such a modality would be, and thus we couldn’t figure out if using such a modality would actually allow us to conclude that certain theories had free models. So we put that aside for the time being.

Computing an appropriate elimination principle for the free models.

With Bob’s help, I was able to do something that I’ve wanted to do for a while but never quite figured out the right induction step for: do a logical-relations style computation of the type of homomorphisms for a theory, e.g. the \(-^M\) part of the AMDS interpretation in Andras’s thesis.

This gives the type of the recursor for a free model of a theory. And I think similar techniques would help build the displayed models and sections of a displayed model, which would allow me to type the inductor for a free model of a theory.

Quite happy to finally get this under my belt, and it’s much easier than I thought it would be!

Potential/Kinetic Types

I ended up implementing potential and kinetic types in the core of the elaborator I’m working on! Haven’t finished synthesis/checking yet, but various other parts (evaluation, reification, etc.) are chugging along smoothly.

Value telescopes

This is a relatively minor detail, but I finally figured out how to do a satisfying definition for semantic telescopes (as would appear in the value of a dependent record type).

Previously, I was doing them in defunctionalized style as a “multi-pronged closure”. That is

data TeleV = TeleV Env [(Name, TyS)]

where TyS is “type syntax”. I think the “functionalized” version makes a variety of operations that I am doing easier, but the naive definition (TyV = type value, ElV = element value)

data TeleV = TNil | TCons Name TyV (ElV -> TeleV)

is annoying because you can’t pull out the list of fields easily. So instead what I do is

data AnonTeleV = TNil | TCons TyV (ElV -> TeleV)

data TeleV = TeleV [Name] AnonTeleV

This assumes that the length of the AnonTeleV is the same as the length of [Name]. Then operations on TeleV essentially unfold both the names and the telescope at the same time, which works pretty smoothly.

SPLS

I got to go to St. Andrews on Wednesday for SPLS, which was very fun! It was great to see so many PL theorists in one room; and I definitely will try to make it to the next one.

Also, nice to see my professor from undergrad Shriram!

MSP Group

Bob is in a wonderful group at Strathclyde, the mathematically structured programming group, and it was great talking with the various PhD students/postdocs/research assistants/lecturers/professors… and in true British fashion giving my liver a workout at the pub every night.