Re: [Epigram] Definitional equality in observational type theory
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
Re: [Epigram] Definitional equality in observational type theory
Hi Robin, I just saw Thorsten answered your e-mail. I'd better finish what I started though. I'm not an expert on OTT, but here are a few thoughts. The "real" rule for coercion is the one on page 3. It doesn't require the types to be definitionally equal. Section 5 mainly speculates on adding two extensions: * Definitional proof irrelevance * Definitionally defining all coherence proofs to be refl and coercions within the same type to be the identity. Like Thorsten says, this is a bit tricky and makes evaluation and equality mutually recursive - which is a bit odd. If you're looking to understand OTT, I wouldn't get too worked up about this rule - it's a bit technical and the really important stuff is in the first few sections. I'm not sure if it helps, but here's a bit of Agda code "implementing" OTT: www.cs.nott.ac.uk/~wss/Misc/ott.agda I certainly understood much more of the paper after writing the Agda. I'm not sure if reading it will have quite the same effect, but it might be worth a shot. All the best, Wouter This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
Re: [Epigram] Definitional equality in observational type theory
Hi Robin, thank you for your comments. Indeed we are currently revising this paper, hence your comments are especially welcome. 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. We should certainly strive to fix this... 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.) You are right to say that this rule is unusual. In the implementation it creates a dependency between defintional equaliy and reduction which doesn't appear in conventional systems. It can be justified by observing that in intensional Type Theory we have tat s [refl S> ≡ s where refl S : S=S. However, due to proof-irrelevance any term Q : S = S will be definitionally equal to refl S, hence if p:S=S then s [p> ≡ s 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. You are right - your rule is equivalent and more concise. However, a type checker will have to implement the first rule. To check whether s [Q> reduces to s you have to verify whether the types in the type of Q:S = T are definitionally equal, i.e. whether S ≡ T. Where have I gone wrong? Indeed nowhere. There is some discussion of related issues in the Epigram developers blog: http://www.e-pig.org/epilogue/ is particular in the Epigram 2 design doc. Cheers, Thorsten This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
