11

But is that exactly where they are located in the lambda cube? The lambda cube is not a giant spectrum on which all programming languages can be classified. It is precisely eight languages, which combine a lambda calculus (values abstracted over values) with all possible combinations of three features: Values abstracted over types (parametric polymorphism) ...


11

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 ...


6

The original conception of propositions-as-types did not distinguish propositions and types at all: all types are propositions. Under this view, we may indeed speak of different proofs of a proposition. One way to understand the differences between different conceptions of propositions-as-types is to view them as capturing different notions of provability ...


6

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)$. ...


5

relational databases are among the highest value, most researched applications of computer science James, what do relational databases have to do with the question? And why have you tagged this q with 'relational-algebra'? It seems to me entirely gratuitous. Just because databases are 'relational' does not mean they have much to do with whatever Russell ...


5

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 ...


5

Yes, there is such an untyped function, and it turns out that it is equivalent to the untyped erasure of iteration for church numerals. The Cedille project has been doing lots to give types to these functions, and the core concept there is the dependent intersection, which provides a limited form of self reference that is enough to derive induction ...


5

In an untyped language, those expressions would be equivalent. When working with types, instead, one might have a type while the other one has no type. Assume that numbers and arithmetic operators all work on $\sf nat$. Then $e_0 = 2+2$ can be typed as $\sf nat$. Now, we can try to perform a $\beta$-expansion, i.e. to "apply $\beta$ backwards", and reach $...


3

Your notation and understanding are pretty good. It is easier to consider (xs:x) as the inductive case instead of (x:xs) \begin{align} \sum_{i:\ 0 \leq i < \#(xs:x)} &(xs:x).i * (i + 1)\\ &=\sum _{i:\ 0 \leq i < \#xs+1} (x:xs).i * (i + 1) \\ &=\sum_{i:\ 0 \leq i < \#xs} (xs:x).i * (i + 1)+\sum_{i:\ i=\#xs}(xs:x).i * (i + 1)\\ &=\...


Only top voted, non community-wiki answers of a minimum length are eligible