We know that the CoC is essentially a calculus combining dependent typing, parametric polymorphism, and type constructors. What exactly do each of these three give us in terms of representation power when we’re writing theorems/proofs?
Parametric polymorphism obviously gives us the forall operator, which is essential for the majority of proofs, but what exactly do dependent types and type constructors give us?
My guess is that dependent types are why we can reason about the output of functions and what they output, which is critical for any correctness proof. I’ve heard that type constructors give us the exists type operator, but I can’t find any reference for that. How far off am I?
As far as I am concerned, the forall quantifier primarily comes from dependent typing, not from parametric polymorphism. Indeed, when you declare foo: forall x:nat, P and then get foo 1: P[1\x], this is plain dependent typing. As for the exists quantifier, it is a type operator, since it takes two types, and it returns a type, so yes. (And by the way, its type is itself a dependent type: exists: forall T:Type, (T -> Prop) -> Prop.)
I see what you’re saying re: forall, you do need a type-to-type function to represent that, which you would get from the Pi abstraction in dependent types. So what does polymorphism get us then? Just slightly more program generality? @silene
If types are terms that can participate in dependent products, then parametric polymorphism does not bring anything to the table, it is just a consequence of dependent typing. So, I suppose you could split dependent typing in two categories, depending on whether it applies to values (e.g., forall x:nat) or to types (e.g., forall T:Type), and define parametric polymorphism as the latter, by opposition to the former. In that case, the ability to give types to type constructors is a consequence of parametric polymorphism, as exemplified by the exists quantifier above, since its type is forall T:Type, (T -> Prop) -> Prop.
But another way to see it is that, as soon as your system of dependent types collapse the type hierarchy (i.e., types are terms), trying to see how the three axes of the lambda-cube fit in there becomes a bit of a pointless exercise.
Thank you, that helped! I was thinking of dependent typing as (term → type) and polymorphism as (type → term), so hadn’t considered that they can both be viewed as parts of a larger single concept. This clarification helped for an intro to FV presentation I gave last night: https://seashell.charles.systems/writings/sotu.pdf