Hi Robin,

`thank you for your comments. Indeed we are currently revising this`

`paper, hence your comments are especially welcome.`

## Advertising

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 itseems silly (apologies if my email client mangles this even after I'vetried to fix it up - I've never tried pasting type rules from PDFsintoit before): Γ |- S≡T Γ |- Q:S=T Γ |- s:S ------------------------------ T Γ |- s[Q>S ≡ s : TIt seems silly to include a definitional equality as a premise,becauseI _thought_ the whole point of definitional equality was that S≡Tmeansthat 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+0the "right" way round! I can't remember offhand which way roundworks.)

`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.