Hi Robin
I was just about to reply when I noticed Thorsten had...
Robin Green wrote:
I've been reading "Towards Observational Type Theory". I'm new to type
theory, so I have not been able to understand big chunks of the paper;
hopefully as I read wider I'll understand more of it.
However, one rule which jumped out at me is this, on page 9, because it
seems silly
Perhaps, but I'm glad you didn't go as far as to say it was wrong.
(apologies if my email client mangles this even after I've
tried to fix it up - I've never tried pasting type rules from PDFs into
it before):
Γ |- S≡T Γ |- Q:S=T Γ |- s:S
------------------------------
T
Γ |- s[Q>S ≡ s : T
That transfer seems to have worked remarkably well.
It seems silly to include a definitional equality as a premise, because
I _thought_ the whole point of definitional equality was that S≡T means
that S and T are freely co-substitutable, and type-checking will
automatically substitute S for T or T for S _whenever_ required.
Thinking back to how and when we wrote this, I can see how it got done
that way. When you write a judgmental equality system for a type theory,
you tend to chuck in
(1) equivalence closure
(2) structural closure (replaced selectively by eta-laws)
(3) the computation schemes
(4) conversion for equality judgments
You then throw in a conversion rule for the typing judgment and write
the rest of your typing rules just as you suggest, as if conversion in
types happens by magic. Flying at top speed on automatic pilot, that's
exactly what we did.
The point about the above rule is that it comes under (3), and it's what
we implemented as part of *evaluation* for OTT. When you're evaluating
coercions, you really have to check the definitional equality of the
types. We didn't take the time to figure out how to hide these
preconditions by exploiting the conversion rule. Conversion-for-free in
the typing rules is normal; conversion-for-free in the computation
schemes is not dissimilar, I suppose, but requires thought. Sometimes,
the typing rules *guarantee* that that the repeated schematic variables
will correspond to definitionally equal terms (eg in the computation
rules for inductive families); here it is actually necessary to *check*.
So anyway, surely any derivation which needed that rule could also
use this rule instead:
Γ |- Q:S=S Γ |- s:S
------------------------------
S
Γ |- s[Q>S ≡ s : S
(which is trivial), substituting S for T before applying it, and
substituting Ts for some of the Ss afterwards.
Yes, you need to use S==T to get s[Q>_S^T == s[Q>_S^S == s, as well as
S=T == S=S for the type of Q.
Where have I gone wrong?
Looks ok to me. But if you asked me to choose, I'd still pick the
presentation of the computation schemes which makes it clearer what
computation actually needs to happen. There's a deeper malaise here
which is hard to pinpoint. The gap between the way we usually have to
present these systems and the way they actually work just keeps on
getting wider. I find it quite depressing, because we have to talk about
what we did in a manner which doesn't really reflect how we did it.
So perhaps it's a question of perspective. Or maybe it is just silly. I
haven't really thought about it enough.
Well, I have for this morning, anyway.
All the best
Conor
