I discuss dependent types, which are types that can contain non-type
programs. An example of a dependent type is a list whose type contains
its length. Instead of just writing List<String> for
a list that contains strings, dependent types include types like
List<String, 5> that describe lists of exactly five
strings. Dependent types...