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.
Asked By : oconnor0
Answered By : jozefg
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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/52314
0 comments:
Post a Comment
Let us know your responses and feedback