Talk:Dependent type
From Wikipedia, the free encyclopedia
 |
This article is within the scope of the WikiProject Philosophy, which collaborates on articles related to philosophy. To participate, you can edit this article or visit the project page for more details. | ||||||||
| ??? | This article has not yet received a rating on the quality scale. | ||||||||
| ??? | This article has not yet received an importance rating on the importance scale. | ||||||||
|
|||||||||
The Type system article describes dependent types as "types which depend on run-time values". This is obviously a computer science oriented definition, but would it be useful to add it to this article? --65.147.3.110 20:08, 10 September 2006 (UTC)
there should also be something about the berendregt cube, \lambdaP, and the relation to other type systems
there should be information about implementation difficulty, undecidability, etc.
Coq is actually based on the Calculus of Constructions (a.k.a. Lambda P Omega), which is a strictly more powerful system than Lambda P. In the traditional orientation of the Barendregt cube, Lambda P forms the front, bottom, right corner, and CC the back, upper, right corner (which corresponds, relative to Lambda P, to the addition of terms depending on types (as in System F) plus types depending on types (as is Lambda Omega / System F Omega)).
[edit] C++ templates
I added C++ templates to the list of supporting languages. I am not sure if this is in accordance with the definition of dependent types, but I decided to wp:be bold. Here is a basic example of an array in C++:
template <class T, int i>
class array {
public:
T elements[i];
};
array<char, 5> foo; // array of 5 char's
