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 op

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.