Universal/existential quantification?

Question

I'm struggling to understand the purpose of universal and existential quantification of types. I'm playing around with writing a toy language based on the calculus of constructions. I've been reading about Morte and Henk to help me get a better understanding.

I don't understand why the CoC has both lambda and forall abstraction.

$$(\lambda x:A . B)$$ $$(\forall x:A . B)$$

It seems to me that lambda subsumes forall in a system where types are passed manually. In other words, that the following

$$(\forall x : *. \lambda a : x. a)$$

Could be replaced with

$$(\lambda x : *. \lambda a : x. a)$$

If it was first applied to the type being used.

What am I missing? What papers or blogs or articles are there to read that might help me?

Thanks.

Answer 1

It helps to remember that $\forall$ (or $\Pi$ as you sometimes see) is a type. It's generalizing $\to$. So while it makes perfect sense to say $(\lambda x : A. M)\ N$, it doesn't make sense to say $(\forall x : A. M)\ N$ because $\forall ...$ is just a type. You wouldn't say $(A \to B)\ N$ becaues $\to$ isn't for computing per-se, it's there to classify lambda terms which can be applied like this.

This was something that tripped me up as well, but this is how the calculus of constructions (as well as any other dependently typed system is defined).

The two programs you wrote have very different intentions and the first one is ill-typed. It doesn't make sense to say $\forall x : A.\ \lambda x.\ x$ because $\forall$ requires both its arguments by types which means that if $\forall x : A. B$ is to be well-typed, we must have $B : *$. However, $\lambda x. x$ isn't a type, it can only ever be assigned a type of the form $\forall x : A. B$, never $*$. The second one on the other hand is almost (I think you meant to return $a$ not $x$) is a function and is given a type using two $\forall$s.

Answer 2

Keep in mind that existential and universal types are rather different. It is constructive logic, not classical logic and in constructive logic $\forall$ and $\exists$ are not as related as they are in classical logic.

$\forall x:A. B(x)$ is the type of programs that receive an object of type $A$ and return an object of type $B(x)$. The important thing here is that the type $B(x)$ depends on $x$ and is not the same for all $x$. It can vary depending on what $x$ is. For one input $x$ we might output an integer. For another one we might output a real number. For yet another one we might output a function over real numbers. If $B(x)$ doesn't vary with $x$ then you can use $A\to B$ in place which is the type of functions from $A$ to $B$.

$\exists x:A. B(x)$ is the dependent version of (constructive) disjunction. You can think of constructive disjunction $A \lor B$ of two types $A$ and $B$ as the disjoint union of $A$ and $B$. $\exists x:A.B(x)$ is the disjoint union of a collection of types $B(x)$ indexed by $x:A$. The fact that the type $B(x)$ van vary depending on the value of $x:A$ makes it a dependent type. Compare with the case where $B$ does not depend on $x:A$: $\exists x:A. B$. We are taking one copy of the same $B$ for each $x:A$. This is isomorphic to $A \times B$.

Now you can ask why we need dependent product and sum types? Because they give us more expressive power. Now we can ignore the types completely and have untyped type theory/functional programming. But that removes the benefits of having types in the first place, e.g. you will not know if all programs will always terminate (strong normalization). See Lambda Cube and Dependent Type. I think a good way to understand dependent types well is to look at the rules for introducing and eliminating the dependent types in Martin-Lof's type theory.

The main point of dependent types is: we want to remain inside a nice typed theory for various reason (e.g. avoiding bugs, automatic proof of termination, etc.). We don't want to go to something like untyped lambda calculus where we can make expressing like those you stated and way more powerful stuff. We can say that dependent types were invented to allow expressing more things while still remaining inside a nice type theory.