[nbouscal]

The article unfortunately does quite a poor job of explaining what dependent types are and why they're valuable. They're a lot more complicated than just "storing the length of a vector in its type". Dependent types allow you to create types where one type in a signature 'depends' on the value of another type in the same signature. This is very powerful, but unfortunately easily understandable examples are still somewhat hard to come by.