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.