3
$\begingroup$

I'm going through "Type Theory and Formal Proof" by Nederpelt and Geuvers and just trying to play around with $\lambda\underline\omega$ after reading the chapter on it to better grasp the material. The text is a bit vague on some formalities, so I have a couple of questions.

Consider the term $t = \lambda x : ((\lambda \alpha : *. \alpha) nat). x$ (assuming $nat : *$ is in context). Can type-level abstractions and applications be used like this under lambda abstraction type annotations? So, is $t$ a valid term?

If it is, then clearly its type is $(\lambda \alpha : *. \alpha) nat \rightarrow (\lambda \alpha : *. \alpha) nat$, which is $\beta$-equivalent to $nat \rightarrow nat$. But how does $t$ relate to $\lambda x:nat.x$? In other words, can $\beta$-reduction be done under the lambda abstraction type annotation?

$\endgroup$
  • $\begingroup$ What do $nat$ and $*$ denote here? $\endgroup$ – Berci Dec 26 '18 at 2:34
  • $\begingroup$ $nat$ is some type of the kind $*$, and $*$ is, well, the kind of usual types (the ones you'd also encounter in STLC). $\endgroup$ – 0xd34df00d Dec 26 '18 at 2:36
  • $\begingroup$ Ah, so you want a 'varying type' or some, i.e. a lambda expression for the type part (after the colon). I think it has another formalism on that part (maybe 'dependent types') and lambda expressions are only for terms.. But I'm not a lambda calculus expert.. $\endgroup$ – Berci Dec 26 '18 at 3:24
  • $\begingroup$ Yep, that's types dependent on types (basically STLC lifted to the type level). $\endgroup$ – 0xd34df00d Dec 26 '18 at 4:25

Your Answer

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

Browse other questions tagged or ask your own question.