[eximius]

Basically the length of the vector is encoded at the type level. Lets you do all sorts of cool stuff.

You can have number systems modulo n, which are only compatible with other numbers modulo the same n because they are distinct types.

It's just another level of abstraction that pretty much nothing else has.