Chapter 4: Programming with GADTs
The fourth chapter of the Iowa Type Theory Commute is about a special
case of dependent types known as Generalized Algebraic Datatypes (GADTs).
These allow you to form datatypes with indices like n in Vector n that vary as you
descend into the value of the datatype. Vector is a classic example, where n is the
length of the vector, and it decreases as you dig down into the Vector.