Dependent types

So, why are you not using dependent types yet? Do you like your programs randomly crashing?

>>6
The idea is basically that types may depend on values, so you can have something like List 50 Int for the type of a list with 50 elements. A functions like head that take the 1st element of a list could have a type like {t : Type} -> {length : t} -> (value : t) -> List (1 + length) t -> t
(the arguments in {} can automatically be deduced by the compiler)
And you get:
head (cons 9 nil) = 9
head nil = compile time type error as the type of nil is something like List 0 Int
That way you basically can't do things like int sussman[10]; sussman[90] = 100;