19
$\begingroup$

The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems to result in a relatively straightforward union (maybe I'm missing something?). But when I look at the CoC, instead of looking like a combination of all three, it looks like a completely different thing. Which dimension do Type, Prop, and small/large types come from? Where did dependent products disappear to? And why is there a focus on propositions and proofs instead of types and programs? Is there something equivalent that does focus on types and programs?

Edit: In case it isn't clear, I'm asking for an explanation of how the CoC is equivalent to the straightforward union of the Lambda Cube dimensions. And is there an actual union of all three out there somewhere I can study (that is in terms of programs and types, not proofs and propositions)? This is in response to comments on the question, not to any current answers.

$\endgroup$
  • 1
    $\begingroup$ At the very least this should be a soft-question. I do not see an actualy technical question here. Perhaps you can be a bit more specific as to what you're asking? $\endgroup$ – Andrej Bauer Jun 27 '16 at 9:40
  • 3
    $\begingroup$ @AndrejBauer Isn't the question: What is the relationship between the Barendregt-cube/PTS presentation of the CoC and the original presentation by Coquand & Huet? $\endgroup$ – Martin Berger Jun 27 '16 at 12:21
  • 1
    $\begingroup$ @AndrejBauer : The question also seems to be asking about the difference in the presentation of CoC (in either guise) and the emphasis on certain features in practice. It is true that the PTS-oriented version of CoC emphasizes some features as important, while the practice of Coq emphasizes others. I do agree that it ought to have the soft-question tag. $\endgroup$ – Jacques Carette Jun 27 '16 at 12:24
  • 1
    $\begingroup$ I am glad to see someone will be able to answer this. $\endgroup$ – Andrej Bauer Jun 27 '16 at 14:53
27
$\begingroup$

First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is based on) is very different from the Calculus of Constructions. It is best thought of as starting at Martin-Löf type theory with universes, and then adding a sort Prop at the bottom of the type hierarchy. This is a very different beast than the original CoC, which is best thought of as a dependent version of F-omega. (For instance, CiC has set-theoretic models and the CoC doesn't.)

That said, the lambda-cube (of which the CoC is a member) is typically presented as a pure type system for reasons of economy in the number of typing rules. By treating sorts, types, and terms as elements of the same syntactic category, you can write down many fewer rules and your proofs get quite a bit less redundant as well.

However, for understanding, it can be helpful to separate out the different categories explicitly. We can introduce three syntactic categories, kinds (ranged over by the metavariable k), types (ranged over by the metavariable A), and terms (ranged over by the metavariable e). Then all eight systems can be understood as variations on what is permitted at each of the three levels.

λ→ (Simply-typed lambda calculus)

 k ::= ∗
 A ::= p | A → B
 e ::= x | λx:A.e | e e

This is the basic typed lambda calculus. There is a single kind , which is the kind of types. The types themselves are atomic types p and function types A → B. Terms are variables, abstractions or applications.

λω_ (STLC + higher-kinded type operators)

 k ::= ∗ | k → k
 A ::= a | p | A → B | λa:k.A | A B
 e ::= x | λx:A.e | e e

The STLC only permits abstraction at the level of terms. If we add it at the level of types, then we add a new kind k → k which is the type of type-level functions, and abstraction λa:k.A and application A B at the type level as well. So now we don't have polymorphism, but we do have type operators.

If memory serves, this system does not have any more computational power than the STLC; it just gives you the ability to abbreviate types.

λ2 (System F)

 k ::= ∗
 A ::= a | p | A → B  | ∀a:k. A 
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Instead of adding type operators, we could have added polymorphism. At the type level, we add ∀a:k. A which is a polymorphic type former, and at the term level, we add abstraction over types Λa:k. e and type application e [A].

This system is much more powerful than the STLC -- it is as strong as second-order arithmetic.

λω (System F-omega)

 k ::= ∗ | k → k 
 A ::= a | p | A → B  | ∀a:k. A | λa:k.A | A B
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

If we have both type operators and polymorphism, we get F-omega. This system is more or less the kernel type theory of most modern functional languages (like ML and Haskell). It is also vastly more powerful than System F -- it is equivalent in strength to higher order arithmetic.

λP (LF)

 k ::= ∗ | Πx:A. k 
 A ::= a | p | Πx:A. B | Λx:A.B | A [e]
 e ::= x | λx:A.e | e e

Instead of polymorphism, we could have gone in the direction of dependency from simply-typed lambda calculus. If you permitted the function type to let its argument be used in the return type (ie, write Πx:A. B(x) instead of A → B), then you get λP. To make this really useful, we have to extend the set of kinds with a kind of type operators which take terms as arguments Πx:A. k , and so we have to add a corresponding abstraction Λx:A.B and application A [e] at the type level as well.

This system is sometimes called LF, or the Edinburgh Logical Framework.

It has the same computational strength as the simply-typed lambda calculus.

λP2 (no special name)

 k ::= ∗ | Πx:A. k 
 A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A [e]
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

We can also add polymorphism to λP, to get λP2. This system is not often used, so it doesn't have a particular name. (The one paper I've read which used it is Herman Geuvers' Induction is Not Derivable in Second Order Dependent Type Theory.)

This system has the same strength as System F.

λPω_ (no special name)

 k ::= ∗ | Πx:A. k | Πa:k. k'
 A ::= a | p | Πx:A. B | Λx:A.B | A [e] | λa:k.A | A B 
 e ::= x | λx:A.e | e e 

We could also add type operators to λP, to get λPω_. This involves adding a kind Πa:k. k' for type operators, and corresponding type-level abstraction Λx:A.B and application A [e].

Since there's again no jump in computational strength over the STLC, this system should also make a fine basis for a logical framework, but no one has done it.

λPω (the Calculus of Constructions)

 k ::= ∗ | Πx:A. k | Πa:k. k'
 A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A [e] | λa:k.A | A B 
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Finally, we get to λPω, the Calculus of Constructions, by taking λPω_ and adding a polymorphic type former ∀a:k.A and term-level abstraction Λa:k. e and application e [A] for it.

The types of this system are much more expressive than in F-omega, but it has the same computational strength.

$\endgroup$
  • 3
    $\begingroup$ Of course, technically CoC (without axioms) has at least as many set-theoretic models as the CiC, they just aren't very good at modelling the situation we want, which is the CoC with axioms for the natural numbers (say, $0 \neq 1$). $\endgroup$ – cody Jun 29 '16 at 12:21
  • 2
    $\begingroup$ I'd also really appreciate a reference on the conservativity of $\lambda\omega\_$ over the STLC. This seems non-obvious. $\endgroup$ – cody Jun 29 '16 at 12:23
  • 3
    $\begingroup$ @cody: I don't know a reference -- Kevin Watkins sketched the proof for me on a whiteboard! The idea is that you take a term typed in λω_, put all the types into beta-normal eta-long form, and then embed it into STLC by introducing a fresh atomic type for each distinct normal form in the original program. Then it's obvious the reduction sequences must line up one-to-one. $\endgroup$ – Neel Krishnaswami Jun 29 '16 at 13:16
  • $\begingroup$ It's probably useful to note that type level variables can't get instantiated by new terms at reduction time, like in $F_\omega$, in which this proof shouldn't work. $\endgroup$ – cody Jun 29 '16 at 17:57
  • 1
    $\begingroup$ @user833970 the fact that $0\neq 1$ is not derivable is actually much more simple than those other facts you mention, and has nothing to do with the encoding of $\mathrm{nat}$: it comes from the fact that there is a proof irrelevant model of CC, in which types have at most one element. This is a bad property if you want a logic in which there is a type with more than one element (say, nat). A reference is: The not so simple proof irrelevant model of CC, by Miquel and Werner. $\endgroup$ – cody Dec 18 '17 at 20:39
21
$\begingroup$

I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot.

But first, one should probably try to dis-entangle various issues. The Coq interactive theorem prover is based on an underlying type theory, sometimes lovingly called the calculus of inductive constructions with universes. You'll note that this is more of a mouthfull than simply "Calculus of Constructions", and indeed, there are a lot more things in there than just the CoC. In particular, I think you're confused about exactly which features are in CoC proper. In particular, the Set/Prop distinction and universes do not appear in CoC.

I won't give a full overview of Pure Type Systems here, but the important rule (for functional PTSes like the CoC) is the following

$$\frac{\Gamma\vdash A:s\qquad \Gamma,x:A\vdash B:k}{\Gamma\vdash \Pi x:A.B\ :\ k}\ (s,k)\in R $$

where $s,k$ are elements of a fixed set $S$ of sorts, and the pair $(s,k)$ is in a fixed set $R$ of pairs of $S$, called the rules.

The crucial insight is that careful choices of $S$ and $R$ make huge differences in what the product type $\Pi x:A.B$ actually represents!

In particular, in the calculus of constructions, the set of sorts $S$ is $$ \{*, \square\}$$ Often called Prop and Type (though this terminology is a bit confusing to a Coq user for reasons I'll talk about later), and the full set of rules: $$R=\{(*,*),(\square,\square),(\square,*),(*,\square)\} $$

And so we have 4 rules which correspond to 4 different purposes:

  • $(*,*)$: Function types

  • $(\square,\square)$: Type families, or types with parameters

  • $(\square,*)$: Polymorphic types

  • $(*,\square)$: Dependent types

I'll explain each of these in more detail.


First note that I'll write $A\rightarrow B$ instead of $\Pi x:A.B$ when $x$ doesn't appear in $B$. This notation is much more suggestive, but can hide some important intuition.

Function types: elements of type $*$ are the "ordinary" types and propositions. They would include $\mathrm{nat}$, $\mathrm{bool}$, and things like the proposition $x=y$ for $x$ and $y$ of a given type. In the CoC. these "basic types" and propositions are all mixed together, as they still are in systems like Agda. Coq tends to separate them into two sorts, often called Set and Prop or Type and Prop. This facilitates extraction, and allows us to assume proof irrelevance for things in Prop if we want to (we definitely don't want it for things in Set). The ability to form pi-types at sort $*$ gives us the usual higher-order functions you enjoy in any functional programing language, i.e. the ability to pass functions into other functions.

Type families: This gives you the ability to talk about the familly $\mathrm{list}$ on its own, indeed as a well typed term $\mathrm{list}:*\rightarrow *$, rather than just the instances $\mathrm{list}_{\mathrm{nat}}, \mathrm{list}_{\mathrm{bool}}$, etc. Note that simply forming the type $*\rightarrow *$ requires using the $(\square,\square)$ rule.

Polymorphism: This is controversial, but very useful, and a source of great power in the CoC. The usual motivation is the desire to write the type $$\Pi t:*.\ t\rightarrow t $$ to be able to type the polymorphic identity $\lambda (t:*)(x:t).x$. Here the quantification $\Pi t:*.\_$ is possible thanks to the $(\square, *)$ rule (though the $t\rightarrow t$ only uses the $(*,*)$ rule).

But it's an interesting fact that we can express all the usual logical operators using this quantifier! Here are a few: $$A\wedge B := \Pi t:*.\ (A \rightarrow B\rightarrow t)\rightarrow t$$ $$A\vee B := \Pi t:*.\ (A \rightarrow t)\rightarrow(B\rightarrow t)\rightarrow t$$ $$\bot := \Pi t:*.\ t$$ $$\top := \Pi t:*.\ t\rightarrow t$$ $$ \exists x:A.\ P(x):= \Pi t:*.\ (\Pi y: A.\ P(y)\rightarrow t)\rightarrow t$$ That last one actually also uses dependent types (the $(*,\square)$ rule), but this should give you an idea of the power of polymorphism.

In fact, polymorphism is so powerful, that adding inductive types with "large elimination" (the ability to define things in $*$ by recursion) implies the excluded middle is inconsistent with the excluded middle! That's why in Coq, Prop (the analogue of $*$) has some restrictions: no large eliminations, and datatypes should live in Set or Type, which don't have the analogue of the $(\square, *)$ rule. Prop without large eliminations is consistent with the law of excluded middle.

Useful to note: in the presence of $(\square,\square)$, you can even write things like: $$\Pi c:*\rightarrow *.\ \ c\ \mathrm{nat}\rightarrow c\ \mathrm{nat} $$ if you like, which is useful for, say, writing generic code over a monad, as often happens in Haskell.

Dependent types: This is how you get the propositions-as-types paradigm to work. Indeed, you want to have a type that represents all possible proofs of, say $0=1$. To make sense of this, you want equality to be of type $$ =\ :\ \mathrm{nat}\rightarrow\mathrm{nat}\rightarrow *$$ or you might want to be polymorphic $$ =\ :\ \Pi t:*.\ t\rightarrow t\rightarrow *$$ In any case, you can't write $\mathrm{nat}\rightarrow\mathrm{nat}\rightarrow *$ without the rule $(*,\square)$.

Ok, but what about universes? It turns out that in the CoC, you can't actually write things like $\square \rightarrow \square$, because there are no types to give $\square$ and a fortiori no rules involving those types. A pretty natural thing to do is to index $\square$ by a natural number, getting $\square_i$ for $i=1,2,3,\ldots$ and having $\square_i:\square_{i+1}$.

What rules do we want for this? One natural rule is $(\square_i, \square_i)$, but that rule isn't very useful in the absence of the subsumption rule $$ \frac{\Gamma\vdash A:\square_i}{\Gamma\vdash A:\square_j}\ i\leq j$$

With these extra sorts and rules, you get something that is not a PTS, but something close. This is (almost) the Extended Calculus of Constructions, which is closer to the basis of Coq. The big missing piece here is the inductive types, which I won't discuss here.

Edit: There's a rather nice reference that describes various features of programing languages in the framework of PTSes, by describing a PTS which is a good candidate for an intermediate representation of a functional programing language:

Henk: A Typed Intermediate Language, S. P. Jones & E. Meijer.

$\endgroup$
  • 2
    $\begingroup$ Advanced Topics in Types and Programming Languages, S2.6 and S2.7. $\endgroup$ – Kaveh Jun 28 '16 at 7:02
  • 2
    $\begingroup$ BTW "Type families" are often also called higher-kinded types. $\endgroup$ – Martin Berger Jun 28 '16 at 10:28

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.