Statically typed linear algebra in Haskell

ABSTRACT

Numerical computations are often specified in terms of operations on vectors and matrices. This is partly because it is often natural to do so; but it is also partly because, being otherwise useful, such operations have been provided very fast implementations in linear algebra libraries such as ATLAS (implementing BLAS), LAPACK, fftw, etc. Due to their better cache awareness and use of specialized processor instructions, a high-level invocation of an operation such as matrix multiplication using these libraries may execute orders of magnitude more quickly than a straightforward low-level implementation written in, say, C. The combination of efficiency and expressivity has made the framework of linear algebra an exceedingly popular one for scientists. For example, Matlab[1], an interpreter of a simple linear algebra language, has become a standard research tool in many fields.The process of expressing an algorithm in terms of matrices can be error-prone. Matlab and other popular matrix languages are dynamically-typed, which means that type errors are only detected at run-time. Even statically typed languages rarely keep track of more information in an object type than its tensor rank (e.g., to discriminate between matrices and vectors) and element type.If we could additionally expose object dimensions to the type system then we would ideally be able to detect a much wider variety of common errors at compile time than is currently possible. This would in turn make it easier to build and maintain larger numericsintensive software projects.We call our idea of exposing dimensions to the type system "strongly typed linear algebra". We have written a prototype implementation in Haskell, which is based on Alberto Ruiz's GSLHaskell[2] and which uses techniques from Kiselyov and Shan's "Implicit Configurations" paper[3].The presentation will cover the key aspects of our design such as the use of GADTs to combine matrix and vector types, and the use of higher-rank types and staging (namely, Template Haskell) to closely approximate a dependent-type system. Then, we will give a demonstration of interactive use, and compare our system to existing systems in the areas of speed and usability.

REFERENCES

• 1: Matlab. http://www.mathworks.com/.
• 2: A. Ruiz. Matrix computations in haskell based on the gsl. http://dis.um.es/~alberto/GSLHaskell/matrix.pdf, June 2005.
• 3: Oleg Kiselyov , Chung-chieh Shan, Functional pearl: implicit configurations--or, type classes reflect the values of types, Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, September 22-22, 2004, Snowbird, Utah, USA [doi>10.1145/1017472.1017481]
• 4: SciViews. http://www.sciviews.org/benchmark/index.html, August 2003.
• 5: J.W. Eaton. GNU Octave: a high-level interactive language for numerical applications. GNU/Free Software Foundation, Boston, 1998.
• 6: F. Eaton. Statically typed linear algebra in haskell (papers and sourcecode). http://ofb.net/~frederik/stla/, July 2006.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism; Abstract data types

General Terms:
Design, Languages

Keywords:
existential types, higher-rank polymorphism, linear algebra, staging, template Haskell