The Iowa Type Theory Commute, Chapter 4

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.