Are generics parameterized by values the same as dependent types?

Question

I've been reading up on dependent types and I have one question to make sure I'm not misunderstanding something. The Wikipedia page on dependent types starts with this:

In computer science and logic, a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value.

---

Suppose I have a language where I can represent a number in a range:

struct Int<Min, Max>

For example, the type Int<0, 10> represents an integer between 0 inclusive and 10 exclusive.

As a bonus, suppose I introduce generic variance:

struct Int<in Min, out Max>

For example, instances of types such as Int<3, 10> and Int<0, 8> can be assigned to variables of type Int<0, 10>.

Now the addition operation on this type could have a signature like this:

Int<Min1 + Min2, Max1 + Max2> operator+(Int<Min1, Max1> op1, Int<Min2, Max2> op2);

So, adding an Int<0, 10> and an Int<3, 4> would produce a result of type Int<3, 14>.

In such a type system, we could also have ordered pairs, such as:

struct OrderedPair<Min, Mid, Max>
{
    Int<Min, Mid> SmallerNumber;
    Int<Mid, Max> LargerNumber;
}

And so on.

---

Is this different from dependent typing? If so, how?

Answer 1

This is a limited form of dependent typing, in which types can depend on values, but those values must be available at compile time.

In a fully dependently typed language such as Idris, types can also depend on runtime values—in order to construct such a value, you need a proof in scope that the value inhabits the type. One way to obtain a proof is with a simple test (pseudocode):

m = user_input();
n = user_input();

// Type error: n is not guaranteed to be in range.
x = Int<0, m>(n);

if (n >= 0 && n <= m) {
  // Accepted: proofs of n >= 0 and n <= m in scope.
  x = Int<0, m>(n);
}

So you can implement your example in (say) C++, but constructing an Int<Min, Max> requires a dynamic check in the constructor; if C++ had full dependent types, you couldn’t even call the constructor without some form of check (static or dynamic).