Recent correspondence on the mailing list got me to thinking about OTT, proof irrelevance and what have you. I think, but am not yet sure, that we may be able to avoid deciding conversion during evaluation after all. This would really clean things up very nicely if true. What have we?
- Evaluation from terms to values. We rely on this having the ‘Geuvers Property’, namely that any term equal to a canonical term will compute to a canonical value with the same head. Typechecking matches on canonical types; evaluation matches on canonical values.
- Type-directed value conversion. We decide equality by comparing values of known type, matching on the value of the latter in order to perform η-expansions as required.
- Type-recovering neutral conversion. We decide equality of neutrals (in proof-relevant types) by comparing their neutral components, recovering sufficient type information to see how to compare their value components. E.g., references are compared by name and can be typed directly from the information cached along with the name; to compare neutral applications, first compare the neutral functions, then use their recovered type to see how to compare the argument values and recover the type of the whole.
- Quotation of typed values to checkable terms and of arbitrary neutrals to terms with inferrable types. This is how we get sensible syntax back out from our semantic representation of values.
Now, the latter three need a name supply in order to go under binders, but what about evaluation? Evaluation certainly needs a name supply if it performs conversion tests, and it would need to perform conversion tests if it were to implement, say, a proof-irrelevant version of the traditional identity type or JMeq. We’d want subst x y q P p to reduce to p for any q equal to (refl x), but that’s any q at all if x is definitionally equal to y. Hence the plumbing of a name supply through Epigram 2’s computation mechanism. We were thinking of OTT as delivering proof-irrelevance plus extensionality.
But it now seems to me that OTT delivers just enough proof-irrelevance anyway, shifting the conversion test which unblocks coercion-by-reflexive-equation from evaluation into both the neutral conversion test and quotation, where there’s a handy name supply anyway. The key point is the way coerce S T Q s (of type T when Q : S = T and s : S) computes. As well as having the proof-irrelevance rule, making coerce S T Q s ≡ s whenever S ≡ T, we also have structural rules which push the coercion under the head of s whenever s is canonical and S and T are canonical with the same head.
When is coerce S T Q s equal to something with a canonical head? Firstly, s must equal something with a canonical head, and secondly, the coercion must compute. So we know S and T compute to types with the same canonical head, hence the coercion can compute under the head by the structural rule. The Geuvers Property appears to hold without the need to use proof-irrelevance. We only appear to need p-i when s is neutral, so we can build simplification by p-i just for neutral s into the neutral conversion test instead. Adding it to quotation also suppresses pointlessly periphrastic neutral terms.
If this is true, it’s rather good news. We get to disentangle evaluation from conversion, and our semantics stops being muddied by the need to work in the Kleisli category of the namespace monad. It will hopefully become clearer how to do the metatheory, too.
Accordingly, I’m trying to put together a toy no-frills implementation of OTT built this way, to see what we can see. And to see if I can still write programs after so long as a yo-yo. Watch this space, and don’t hesitate to get in touch if there’s something really dumb that I’m missing.