From fast exponentiation to square matrices: an adventure in types

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.

REFERENCES

• 1: Richard S. Bird , Lambert G. L. T. Meertens, Nested Datatypes, Proceedings of the Mathematics of Program Construction, p.52-67, June 15-17, 1998
• 2: Richard S. Bird , Ross Paterson, de Bruijn notation as a nested datatype, Journal of Functional Programming, v.9 n.1, p.77-91, January 1999 [doi>10.1017/S0956796899003366]
• 3: F. Warren Burton , John (Yannis) G. Kollias, Functional Programming with Quadtrees, IEEE Software, v.6 n.1, p.90-97, January 1989 [doi>10.1109/52.16906 ]
• 4: Jeremy D. Frens and David S. Wise. Matrix inversion using quadtrees implemented in gofer. Technical Report 433, Computer Science Department, Indiana University, May 1995.
• 5: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 6: Ratf Hinze. Polytypic functions over nested datatypes (extended abstract). In Latin-American Conference on Functional Programming, March 1999.
• 7: Anne Kaldewaij , Victor J. Dielissen, Leaf trees, Science of Computer Programming, v.26 n.1-3, p.149-165, May 1996 [doi>10.1016/0167-6423(95)00026-7 ]
• 8: Chris Okasaki, Purely functional data structures, Cambridge University Press, New York, NY, 1998
• 9: Simon Peyton Jones et al. Haskell 98: A non-strict, purely functional language. http://haskell, org/onlinereport/, February 1999.
• 10: Hanan Samet, The Quadtree and Related Hierarchical Data Structures, ACM Computing Surveys (CSUR), v.16 n.2, p.187-260, June 1984 [doi>10.1145/356924.356930]
• 11: David S. Wise. Matrix algorithms using quadtrees. Technical Report 357, Computer Science Department, Indiana University, June 1992.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Control structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs

General Terms:
Languages, Measurement, Theory