From fast exponentiation to square matrices

Publisher Website
Google Scholar
Abstract
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 individual 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 systems---it uses nested types, polymorphic recursion, higher-order kinds, and rank-2 polymorphism.

This publication has 5 references indexed in Scilit: