# What is the difference between ∀ and Π in the Calculus of Constructions?

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?

• Section 3 of the paper gives the syntax and semantics of the language - this should answer the question as to how these two constructs differ. Perhaps you could make this question less open-ended by asking a specific question about the aforementioned semantics. It seems to me like Forall ranges over kinds only, whereas Pi can range over types as well as kinds (section 3.1). – user2407038 Dec 11 '15 at 8:54
• ∀ is from The Implicit Calculus of Constructions. ∀P :Nat→∗. should be parsed as ∀(P :Nat→∗). (although it seems a bit strange to me to make P 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. – user3237465 Dec 11 '15 at 9:34
• Based on the examples you give, $\forall$ quantifies over types and $\Pi$ quantifies over values. – Dave Clarke Dec 12 '15 at 15:01

I had only a quick and cursory look at the paper — so take this with great care.

It appears that $\Pi X$ is used to express dependent products as in the calculus of constructions. Instead, $\forall X$ looks more like polymorphic types in ML.

The main difference is that, if $t : \Pi x. P(x)$ then $t T : P(T)$, while if $t : \forall x. P(x)$ then $t : P(T)$. Note that the former requires an additional argument, the second does not: the polytype gets instantiated automatically. Rules $\mathit{App}$ and $\mathit{Inst}$ at page 7 cause this difference.

Of course, this also means that introducing $\Pi$ requires a lambda, while introducing $\forall$ does not.

There also is some type / kind distinction related to this, but I can't comment on that precisely.

• Perhaps the forall is for parameters and the pi for indices? – dfeuer Dec 10 '15 at 23:14
• Wait so there are many different versions of CoC itself? – MaiaVictor Dec 11 '15 at 0:46
• @Viclib This paper proposes its own calculus, which differs from CoC, despite borrowing many ideas from it. – chi Dec 11 '15 at 10:25