From fast exponentiation to square matrices: An adventure in types

Square matrices serve as an interesting case study in functional programmin g. Common representations, such as lists of lists, are both inefficient-at least for access to individual elements-and error-prone, because the compil er cannot enforce "squareness". Switching to a typical balanced-tree repres entation solves the first problem, but not the second. We develop a represe ntation that solves both problems: it offers logarithmic access to each ind ividual element and it captures the shape invariants in the type, where the y can be checked by the compiler. One interesting feature of our solution i s that it translates the well-known fast exponentiation algorithm to the le vel of types. Our implementation also provides a stress test for today's ad vanced type systems-it uses nested types, polymorphic recursion, higher-ord er kinds, and rank-2 polymorphism.