Dependent Types in the Purest Form

Community
6

@c-cube: There are many variations and extensions of the calculus of constructions possible. I would mention the following:

  • Martin-Löf’s type theory (MLTT): He introduced the cumulative hierarchy of sorts Type 0, Type 1, Type 2, .... As opposed to the calculus of constructions there is no impredicative sort P. Without impredicativity it is not possible to express recursion directly. You need other means like recursors or inductive constructions.

  • Zhaohui Luo’s extended calculus of constructions (ECC): The extended calculus of constructions has an impredicative sort P and a hierarchy of predicative sorts Type 0, Type 1, Type 2, .... The ECC has all possibilities of CC and MLTT. The proof of strong normalization or consistency as a logic is significantly more complex than the same proof in CC.

I don’t understand your second point. Could you elaborate it more?

Regards
Helmut