$$(abst) \:\frac{\Gamma, x: t_1 \vdash t_2: t_3 \quad \Gamma \vdash (x: t_1) \to t_3: s}{\Gamma \vdash (x: t_1. t_2): (x: t_1) \to t_3}$$

In this rule, why is $(x: t_1) \to t_3$ required to be an inhabitant of some sort? Isn't assuming $t_1: s$ enough?

  • $\begingroup$ ATTaPL requires only $t_1: s$. Not sure if it's rigorous enough. $\endgroup$ – 盛安安 Feb 23 '16 at 15:05

There are two issues here.

The first most obvious one, is that if there is no rule $(s_1,s_2,s)$ in the pure type system, then there is no way to get from the hypotheses $$ \Gamma \vdash t_1:s_1$$ and $$ \Gamma, x:t_1\vdash t_3:s_2$$ to the conclusion $$ \Gamma\vdash (x:t_1)\rightarrow t_3 : s$$ You can see that if there is no such rule, then your hypothesis is insufficient for forming the product type, and therefore you shouldn't be able to form terms of that type. Note that in the Calculus of Constructions, any $s_1, s_2$ has a corresponding $s$ ($=s_2$), so the premisses are sufficient for the conclusion in all cases.

Another, more subtle issue is that even the fact $\Gamma, x:t_1\vdash t_3:s_2$ for some $s_2$ is not obvious from the fact $$\Gamma, x:t_1\vdash t_2:t_3 $$ While actually true, this fact can be subtle to prove depending on how you set up your rules.

The rule you give minimizes the hassle, as it gives you directly the hypothesis that the product is well-formed without having to prove it after the fact.

  • $\begingroup$ In system Fω, $(*, \Box, \Box)$ is not presented. Is'nt banning functions from terms to types in such system the correct behavior? $\endgroup$ – 盛安安 Feb 23 '16 at 16:46
  • 2
    $\begingroup$ Indeed, in $F_\omega$ there is a counter-example to your question: $\mathrm{Nat}:*\vdash (x:\mathrm{Nat}.\mathrm{Nat})\ :\ (x:\mathrm{Nat})\rightarrow *$ is not typeable in $F_\omega$, but would be with your proposed rule. $\endgroup$ – cody Feb 23 '16 at 20:23
  • $\begingroup$ Sure, I'm now convinced. So ATTaPL is wrong D: $\endgroup$ – 盛安安 Feb 24 '16 at 5:45
  • $\begingroup$ I assume you're referring to Advanced Topics in Types and Programming Languages. Could you give the exact reference (page number)? It's possible that, in context, the claim is correct, but is a different statement than you think. $\endgroup$ – cody Feb 24 '16 at 16:26
  • $\begingroup$ Oh, after checking the content again, I found that it's talking about simpler system then CoC, never mind. $\endgroup$ – 盛安安 Feb 25 '16 at 5:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.