observational type theory (the motivation)
The history of typed programming is the history of the struggle for equality. Raising the topic of equality is the single most effective way to start a fight in a room full of type theorists, and you can do it just by casually using the verb “is” — someone will ask you what “is” is, and then the air will fill with custard pies.
Never trust a type theorist who has not changed their mind about equality.
Let’s muck in. As soon as you have any notion of computation in types, you acquire the nontrivial problem of determining when two types are sufficiently alike that a value of one passes as a value of the other. Details vary, but most type theories ensure that a rule like the following is at the very least admissible
G |- s : S G |- S = T : Type ------------------------------------ G |- s : T
where the notion of equality is presented as a judgment. The circumstances under which that judgment holds vary wildly. Different people approach the problem with different priorities and different prejudices. I am no exception.
When you arrive as a foreigner to someone’s local variety of type theory, a key thing to say is “I want to know what the Language Of Verifiable Evidence is. I want you to show me.”. Given a judgment, what is the decidably checkable document that can certify it? I need to know the answer to this question, because I don’t want to have to trust you. Given the set of judgments J, there should be a set E of evidence and I should be able to implement my own total function check : J -> E -> 2 such that
- if check j e = tt, then j holds
- if j holds, then for some e, check j e = tt
Now, there is one obvious candidate for E — the set of derivations for judgments. In this case, check j e need merely confirm that each step of e is valid and that its conclusion is j. However, derivations can be large, especially when they explain every step of computation that has been used to identify types. Systems (e.g., NuPRL) which use derivations as evidence tend to work in an LCF style, with an abstract type of derived judgments, so that E is never reified as a type of concrete objects: it’s emergent from the execution traces of an ML program. There is no “check”: derivations are presented as arbitrary ML programs which can do many worse things than loop; to see if they’re fit for purpose, you need to evaluate them and see if the judgment derived is the one that you wanted.
I belong to the religion of the other extreme, which holds that the only acceptable candidate for E is 1. That is, I think judgments should be decidable without the need for further certification. In some sense, the division of labour between humans and computers is that humans propose judgments for computers to decide. That’s to say I prefer a system with propositions-as-types and proofs-as-programs. If there’s some certifying information required, I want it in the program, not in the derivation of the programs well-typedness.
A digression from this overlong introduction. Different people use the term ‘core’ or ‘kernel’ theory meaning different things, often with separately valid motivations. I expect the “program”, described above, to be an information-rich document, internal to the implementation of the system. I expect this program to be generated by elaboration from user-supplied source code which is rather more terse, e.g., by methods of constraint-propagation in the tradition of Milner. I also expect this program to contain far more information than is needed for its closed run-time execution, necessitating an extraction process, in the tradition of Coq. Moreover, I expect the information added by elaboration to differ significantly from the information removed by extraction: if we are using types effectively, they should drive the elaboration process to deliver details for the extracted code with only a little explicit nudging from us. I am willing to contemplate type systems in which the programs are the post-extraction ‘realisers’ and the evidence which justifies their safety sits in the derivations, but I want to be sure I can generate those derivations mechanically from the well typed terms of a richer language.
But anyway, different approaches to the role and status of the judgments motivate different approaches to equality. If we take a propositions-as-judgments approach, we might incline to want the equality judgment to capture a more ‘mathematical’ equality. If we want judgments to be decidable and think of propositions as types, then it is inevitable that the equality judgment will be both
- a disappointment, in that to remain decidable, it must fail to recognize some equations, and
- an accident, in that it relies on whatever varieties of computational jiggery-pokery have been implemented.
I’m ok with that because I know computers can’t do everything, but I still like them to work as hard for me as I can think to make them.
Given these differing views of the equality judgment, what happens to the equality proposition, by which I mean the equality type? I’ll be clear to write the equality type as ==. If you think of evidence as living in derivations, you can have
G |- a = b : T G |- q : a == b ---------------------- ------------------- G |- refl : a == b G |- a = b : T
meaning that any algorithm seeking to guess a derivation for an equality judgment must invent a term q from nothing — but of course, things don’t work that way and they’re not meant to. (Of course, refl is usually given just as the proof of a == a, but I fused in an appeal to the conversion rule in order to show the symmetry between introduction and elimination.) This is the approach taken in “Extensional” Type Theory, which is so-called because it allows the derivation of extensional equality between functions — functions are equal if they provably agree on all inputs — but it is not the only way to build a type theory with extensional propositional equality, so as a naming, it doesn’t really characterize the key design choice. The rule on the right is often called the equality reflection rule, and that’s the key characteristic.
The other popular approach, taken by “Intensional” Type Theory, makes == inductively generated by refl, which forces == to characterize whatever disappointing accident happens to be implemented by =. The elimination rule for == and its computational behaviour compound this reliance on whatever it is the equality judgment will accept.
eqJ (A : Type) (a : A) (b : A) (q : a == b) (P (c : A) (q : a == c) : Type) (p : P a refl) : P b q eqJ _ _ _ refl _ p = p
The point is that the output, p, if it ever shows up, will be just exactly the input p, without adjustment. For that to be type-preserving, we must ensure that p : P b q, and hence that P a refl = P b q. Fortunately, matching q with refl is a sufficient condition to make q = refl and b = a. (With equality reflection, the existence of q is enough to make the equation typecheck, which means that any old rubbish typechecks when you hypothesize the proof of a false equation, which means that it is not safe to evaluate open terms.) However, the no-adjustment method of computing with equality proofs forces us to rely on the fact that == ultimately boils down to =. Closed values cannot be made equal unless they are judgmentally so. We have closed equality reflection as an admissible rule.
. |- q : a == b ------------------- . |- a = b : T
By canonicity (the fact that closed expressions compute to canonical values), q must compute to refl. By subject reduction, refl typechecks at type a == b. By inversion, a = b must hold. As we cannot decide the extensional equality of functions, to keep = decidable, we cannot make == extensional. Functions are identified up to their implementations, not their observable behaviour.
Or, put a different way, if we want = to be decidable and == to be extensional, then we must give up on the no-adjustment method of computing with equality proofs, and consider instead a mode of computation which transports values between provably equal types even when they are not necessarily equal judgmentally.
In Observational Type Theory, our mission was to introduce just such a mode of computation with proofs of ==, and then to liberalise == with function extensionality, without losing canonicity. We succeeded. I think it should be possible to achieve the same success for Homotopy Type Theory, with its many rich sources of extrajudicial equality. More about OTT tomorrow. I’m currently visiting Nottingham, which had OTT in it back in the day, so it’s on my mind.