Type-level naturals let you express things like "map on a Vector of length n will produce a Vector of length n" and "given an element x and a vector xs of lengt

Type-level naturals let you express things like "map on a Vector of length n will produce a Vector of length n" and "given an element x and a vector xs of length n, cons x xs will produce a Vector of length (n + 1)". Other functions can inspect these nats and prevent you from taking the head of an empty list, as a very basic example.