I've always wanted someone to write a type-safe framework for tensor manipulation that
a) fully leverages first-class types, and
b) is ergonomic

Maybe that someone has to be me; I wrote a proof-of-concept in Idris and used it to implement transformers:
https://github.com/bgavran/TypeSafe_Tensors

It supports standard tensors, and *non-cubical* tensors given by applicative functors, as well tensor indexing.

So if you have a 't : Tensor [BinTree, BinTree] Double' and you index outside of the shape of the tree, you get a *compile-time* error.

Indexing is powered by containers, transposition by Naperian functors, and non-cubical tensors by applicative functors (see https://cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf)

I was surprised how far one can go with this idea, and how pleasant it was in general to implement all of this in Idris.

What all of this does is enable you to implement the *generalised transformers* as described here (https://glaive-research.org/2025/02/11/Generalized-Transformers-from-Applicative-Functors.html) - transformers that operate on not just vectors, but potentially trees, and other structures too.