Are you saying you consider std::array<int, 5> in C++ to be a dependent type? I'm pretty sure it's not right. I'm pretty sure that the "value" in that quote is,

Are you saying you consider std::array<int, 5> in C++ to be a dependent type? I'm pretty sure it's not right. I'm pretty sure that the "value" in that quote is, implicitly, a "runtime value", or "value of a variable", similar to how we often say "type" without saying "type of a variable". This "5" isn't the value of a variable, it's just an expression. If you continue on to the next paragraph on this Wikipedia page, you will read, first: > The return type of a dependent function may depend on the value (not just type) of one of its arguments. For instance, a function that takes a positive integer n may return an array of length n, where the array length is part of the type of the array. second: > A dependent pair may have a second value of which the type depends on the first value. Sticking with the array example, a dependent pair may be used to pair an array with its length in a type-safe way. Generally, it's the same nomenclature as with the explanation of static vs dynamic type systems: in static type systems, types are attributes of variables, functions and expressions, whereas in dynamic type systems types are attributes of values. And in the static type system of C, 5 has type int, because it's an expression. It representing a value is secondary. A side effect of it is: you can write a compile-time constant in C that will overflow its type, because the type is assigned based on the lexical category, not on the value. As far as I understand, in a dependent type system it should be possible to implement a resizable array "std::vector<int, n>", where n is the length of the array (a variable), then write a "concat" function which concatenates two such arrays, and whose return (static) type depends on the lengths of the arrays passed as arguments. This is different than parametric polymorphism, such as the one that C++ has, since we can't know at compile-time all the possible lengths of arrays that we're going to get at runtime. Idris example here: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#vectors https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.h... If someone has a better understanding of the topic, I'd be delighted to be shown wrong.