As I've learned, the Calculus of Constructions has only two binders - $\lambda$ and $\Pi$. Morte, for example, has $\forall$ as a mere alias of $\Pi$. Yet, on the paper Self Types for Dependently Typed Lambda Encodings, there are types such as:
$$\begin{gather} \mathrm{Nat} := \forall X. (X \rightarrow X) \rightarrow X \rightarrow X \\ \mathrm{It} : \forall X. \Pi x : \mathrm{Nat}. (X \rightarrow X) \rightarrow X \rightarrow X \\ \mathrm{Ind} : \forall P : \mathrm{Nat} \rightarrow \mathord{\ast}. \; \Pi x:\mathrm{Nat}. \; (\Pi y:\mathrm{Nat}. (P \, y \rightarrow P (S \, y))) \rightarrow P \, \bar 0 \rightarrow P \, x \end{gather}$$
Notice that the paper uses both $\forall$ and $\Pi$. Moreover, $\forall$ is used both with the syntax $\forall a : b \rightarrow c$ and $\forall a . b$. I can't parse those expressions. What is the difference between $\forall$ and $\Pi$, and how would you express those types on Morte?
∀
is from The Implicit Calculus of Constructions.∀P :Nat→∗.
should be parsed as∀(P :Nat→∗).
(although it seems a bit strange to me to makeP
implicit in this case). Implicit arguments are convenient, but you can express everything with justΠ
— you'll just need a bit more lambdas and applications. $\endgroup$ – user3237465 Dec 11 '15 at 9:34