I see, so in a way it adds nothing more then convenience? In that, you could manually go ahead and create VectorTwo VectorThree, etc. But no one does because its tedious. So now you could instead say the type is (Vector of Two), which would evaluate to VectorTwo.

I'm still unclear how the type system knows that a VectorOne fits in a VectorTwo, and how inference could work at that level.

Also, with dependent types, I'm unclear what you mean with runtime values, if its still type checked at compile time, wouldn't the value need to be there at compile time?

First off, general note to whom it may concern: Down-voting clarifying questions (e.g. the question I'm replying to) seems unhelpful.

It is indeed merely syntactic convenience if all you have are the labels

  type Zero
  type One
  type Two
  ...

If however, you have operations on those labels that are checked by the compiler, then you have what most people think of when they say "type-level programming," which is more than a syntactic convenience. For example, if the compiler recognizes addition of type-level numbers, that is there is a notion of Plus so that

  Plus One Two

unifies with

  Three

then all of a sudden you can do the classic length-indexed demo of length-checked append.

  appendInts: (Vector N Int, Vector M Int) => Vector (Plus N M) Int

again in pseudo-Scala syntax, which you can't do with simply labeling VectorOne, VectorTwo, etc.

Your question about dependent types is the classic one, if I understand it correctly. Namely, what does it mean for a type (a compile-time concept) to depend on a run-time value, if that run-time value almost always (except for literals) doesn't exist at compile time? The answer is that your type signatures usually end up being generic in the run-time value, and then different code paths allow you to add increasingly specific pieces of information to the run-time value. These code paths are fixed at compile time so the compiler is able to use these pieces of information when it type-checks the code.

An example is probably in order.

Let's say you're accepting user input in the form of a vector of integers (and let's ignore how we were able to format stdin into a vector for now). Again we'll use pseudo-Scala syntax.

  val userInput: Vector n Int

Note that here `n` is an Int (e.g. a 5) not a type-level Five since we're back in dependent type land.

Now we might have a function that only works for vectors of exactly length three and generates some string for those vectors.

  myFunction: Vector 3 Int => String

In order to use `myFunction` on `userInput`, we'll need some intermediate function that actually performs a check that `n` is indeed 3.

  checkIf3 : (n: Int) => Either[n != 3, n = 3]

Now we can do the following.

  checkIf3(userInput) match {
    case Right(nWasIndeed3) =>
      // Now the compiler knows that in this code path n is indeed 3
      myFunction(userInput)
    case Left(nWasNot3) =>
      // Throw some error as appropriate
  }

How you actually pass the information in the `Right` branch that `n = 3` to the compiler is implementation specific. Some implementations might decide to special-case equality and have the compiler automatically include that in the compilation process. Others might use some form of implicit arguments to `myFunction` (so that e.g. Vector 3 Int is actually syntactic sugar for (implicit n = 3, Vector n Int)). Hopefully, however, that serves as an understandable overview of what the general approach looks like.

Now if you're familiar with statically typed languages, you might rightly point out that what I've done in this example I could've done with just ordinary non-dependent types. E.g. if I used a type-level `n` instead of a runtime `n`. This is true for single-argument functions, but dependent types start pulling ahead in expressivity when you have multiple arguments that are related to one another.

For example indexing a vector might look like

  getElementAtIdx: (Int, Vector n A) => Option[A]

in a non-dependently typed language because we don't have a way of expressing a (run-time) relationship between the first and second arguments to our function, namely that the first integer must be less than `n`.

With dependent types we can do this by introducing a third argument.

  getElementAtIdx: (idx: Int, Vector n A, idx < n) => Option[A]

Note that we've also added the syntactic ability to bind a type to a variable in a type signature (idx), which is helps us express relationships among different arguments.