I wanted to share a little example I came across while working on one of my Idris libraries. It's matrix multiplication, but from an angle you may not be used to. In particular, though it is written in Idris (a strict language), it composes as well arrays in Haskell or another lazy language thanks to dependent types.
In short, we represent a matrix as a function taking some bounded indices to a value in a field, viz.
data Matrix : (n : Nat) -> (a : Type) -> Type where
MatrixC : (Fin (S n) -> Fin (S n) -> a) -> Matrix n a
(note that Fin (S n) is the type for natural numbers strictly less than n in
Idris).
With totality checking, this gives us exactly the same type safety we would get
from a Vect n (Vect n a).
But we can do better than an array-based approach as well. In
particular, note that this formulation gives us trivial
fusion. transpose (transpose x) will not copy any values into an intermediate
matrix but instead compose two functions.
I think this is pretty cool! It's a concrete example of somewhere that strict languages can make up for some of the lost compositionality by using dependent types. In Haskell, we have some fluidity in that we can consider functions to be like looking up some key in a map; here we show how to recover that lost flexibility. The whole thing is terse too - in under 200 lines we get matrix multiplication, determinants, inverses, etc.
While the performance of this library is not on par with hmatrix, its elegance and type safety make it quite attractive - matrix multiplication is partial, and it is downright easy to make mistakes.
