6
$\begingroup$

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?

|cite|improve this question
$\endgroup$
  • $\begingroup$ 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). $\endgroup$ – user2407038 Dec 11 '15 at 8:54
  • 4
    $\begingroup$ ∀ 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. $\endgroup$ – user3237465 Dec 11 '15 at 9:34
  • $\begingroup$ Based on the examples you give, $\forall$ quantifies over types and $\Pi$ quantifies over values. $\endgroup$ – Dave Clarke Dec 12 '15 at 15:01
6
$\begingroup$

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.

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

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.