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 (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
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. (For
example, it is often noted that Coq will automatically reduce (i.e.
substitute) n+0 to n in a dependent type - but only if you write n+0
the "right" way round! I can't remember offhand which way round works.)
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.
Where have I gone wrong?
--
Robin
