It's significantly different than subclassing. The wikipedia examples are instructive:

  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.

That's a subclass with an object invariant.

(Gotta use the new buzzwords to be l33t. Even for old ideas.)

Sure, so if you use Ada you can write types like this and the runtime will enforce your invariants automatically. What other non-academic languages support that? It’s something I miss from Ada for sure.

You're right in that what's being demonstrated here should actually be old-hat for OO programmers. It's basically a factory that returns things wrapped in an option if pre-conditions fail.

Crucially what's being demonstrated here isn't dependent types at least as they are commonly known (which some of the comments here explain).

Dependent types are when expressions can not only be of a type, but can also return a type.

That means for example something like

    x : (if condition then Boolean else Int)

is a type, i.e. the entire thing within the parentheses to the right of the y.

This is radically different from subclassing. That entire if statement is a type, not just the `Boolean` or `Int` parts.

Indeed because now arbitrary expressions (in particular equality can return a type!) can return types, types can be statements of your program and simply getting the typechecker to accept the type proves properties of your program.

    x : 5 = 5

In here "5 = 5" is a type. This flips normal statically typed programming on its head. We care more about the type than the value! The actual value of "x" is probably not something you care about; it just proves (in this case the trivial statement) that "5 = 5." Less trivial equalities can be stated

    additionCommutes : (a : Int, b : Int) -> a + b = b + a

and proved by providing a value for additionCommutes that satisfies the typechecker. Again the important thing is the entire right-hand-side of additionCommutes is a single type.