One of the things I love about typescript is if your audacious enough you can kind of make some types like this (still a far cry from dependent types):

https://github.com/AKST/analysis-notebook/blob/main/lib/base... (Line 38)

It type checks, but I haven’t gotten a lot of mileage out of this (so far at least). I did something similar for vectors, which has been useful for when I destructure the elements, and it preserves that through vector operations.

https://github.com/AKST/analysis-notebook/blob/777acf427c65c...

The same is actually applies true for matrices, I wrote the multiplication to carry the new size into the output type

https://github.com/AKST/analysis-notebook/blob/777acf427c65c...

That said I mostly use this for square matrixes in web GL so you’re mostly working with square matrixes.

As an aside, this source is from a toy project largely more for leisure and fun, I don’t know if something like this would be suitable for a larger more data oriented project (at least in trend of how I represent data here).