11 ms·
I think you glossed over the point of the article in general. The author isn't asking whether Linear Algebra can be encoded into a static type system, hell, we
by ThatGeoGuy 11y ago
I think you glossed over the point of the article in general. The author isn't asking whether Linear Algebra can be encoded into a static type system, hell, we had Fortran over 50 years ago! What the author is asking is whether the static type system can reasonably check the units of each member within a matrix or vector. Let's go over a short example:
Assume that you have a matrix A, which contains several rows corresponding to measurements, and several columns corresponding to the partials in x (such as in the generic parametric least-squares problem => A * x - b = r, where we want to minimize r^2). What the author is asking is whether or not the static type-checker can manage units and conversions within each element of the matrix. Let's say the first 10 rows of A correspond to units of metres, while the next 10 correspond to angular units (i.e. radians or degrees). The solution of such a system is:
x = -(A' * A)^-1 * A' * b
What the author desires is a way to enforce that the units of the elements of A are maintained, similar to if you had:
LengthInMetres a = LengthInMetres 1 + LengthInInches2;
Where addition between LengthInMetres and LengthInInches would perform the appropriate conversion if need be, or else you would raise an error for a type contract violation. Currently, there isn't any system that encodes the types of each row, column, or even the individual elements within a matrix, which is why the author is raising the question whether or not it's possible for a type system such as Haskell's to do so.
Right now, the best I've seen is linear algebra packages that can template over the internal type, but represents everything as doubles, or a number type of some kind. Numpy has some ability to modify internal data types (such as representing a matrix where each row is a tuple type or some other), but there is:
1. No static enforcement of type contracts in Numpy (more specifically Python)
2. Numpy does not provide the full set of matrix functionality if types are not the standard numeric types (obviously, you can't take the determinant of some arbitrary `object`, even if internally it represents an integer in metres).
Overall, what the author raised is an interesting question, and makes me wonder if we'll ever get to such a point in the future. Of course, seeing as most matrix libraries are built on top of BLAS / ATLAS / LAPACK / MKL, it's doubtful that we'll see any high-performance linear algebra with smart type systems.
EDIT: Formatting