From Fast Exponentiation to Square Matrices: An Adventure in Types

Square matrices serve as an interesting case study in functional programming. Common representations, such as lists of lists, are both inefficient-at least for access to individ ual elements-and error-prone, because the compiler cannot enforce "squareness". Switching to a typical balanced-tree representation solves the first problem, but not the second. We develop a representation that solves both problems: it offers logarithmic access to each individual element and it captures the shape invariants in the type, where they can be checked by the compiler. One interesting feature of our solution is that it translates the well-known fast exponentiation algorithm to the level of types. Our implementation also provides a stress test for todayʹs advanced type systemsit uses nested types, polymorphic recursion, higher-order kinds, and rank-2 polymorphism.