SLAP is a linear algebra library in OCaml with type-based static size checking for matrix operations.
Many programming languages for numerical analysis (e.g., MatLab, GNU Octave, SciLab, etc.) and linear algebra libraries (e.g., BLAS, LAPACK, NumPy, etc.) do not statically (i.e., at compile time) guarantee consistency of dimensions of vectors and matrices. Dimensional inconsistency, e.g., addition of two- and three-dimensional vectors causes runtime errors like memory corruption or wrong computation.
SLAP helps your debug by detecting inconsistency of dimensions
- at compile time (instead of runtime) and
- at higher level (i.e., at a caller site rather than somewhere deep inside of a call stack).
For example, addition of vectors of different sizes causes a type error at compile time, and dynamic errors such as exceptions do not happen. For most high-level matrix operations, the consistency of sizes is verified statically. (Certain low-level operations, like accesses to elements by indices, need dynamic checks.)
This OCaml-library is a wrapper of Lacaml, a binding of two widely used linear algebra libraries BLAS (Basic Linear Algebra Subprograms) and LAPACK (Linear Algebra PACKage) for FORTRAN. This provides many useful and high-performance linear algebraic operations with type-based static size checking, e.g., least squares problems, linear equations, Cholesky, QR-factorization, eigenvalue problems and singular value decomposition (SVD). Most of their interfaces are compatible with Lacaml functions.
$ opam install slap
$ ./configure $ make $ make install
- API documentation: http://akabe.github.io/slap/api/ (generated by
- PPX syntax extensions: http://akabe.github.io/slap/ppx/ (generated by
- Akinori Abe and Eijiro Sumii. A Simple and Practical Linear Algebra Library Interface with Static Size Checking. Proceedings ML Family/OCaml Users and Developers workshops. Electronic Proceedings in Theoretical Computer Science 198, pp. 1-21, 2015. .pdf
The following code (examples/linsys/jacobi.ml) is simple demonstration for static size checking of SLAP. It is implementation of Jacobi method (to solve a system of linear equations). You do not need to understand the implementation.
jacobi a b solves a system of linear equations
a * x = b where
a n-by-n matrix, and
b is a n-dimensional vectors.
Let’s compile and execute this program:
$ git clone https://github.com/akabe/slap $ cd slap/examples/linsys/ $ ocamlfind ocamlc -linkpkg -package slap,slap.ppx -short-paths jacobi.ml $ ./a.out a = 5 1 0 1 3 1 0 1 4 b = 7 10 14 x = 1 2 3 a*x = 7 10 14
x is computed correctly (since
a*x = b is satisfied).
jacobi has the following type:
This means “
jacobi gets a
'n matrix and a
and returns a
'n-dimensional vector.” If you pass arguments that do not
satisfy the condition, a type error happens and the compilation fails.
Try to modify any one of the dimensions of
x in the above code,
and compile the changed code. Then OCaml reports inconsistency of dimensions:
By using SLAP, your mistake (i.e., a bug) is captured at compile time!