Surely most of the time you don’t need program constants? You could already implement a slow matrix multiplication that is well typed in a language like Haskell or OCaml. It would have a type something like:
val matmul : ((float,'a) fixed_length, 'b) fixed_length -> ((float,'c) fixed_length, 'a) fixed_length -> ((float,'c) fixed_length, 'b) fixed_length
(And observe the similarity to function composition too:
val compose : ('a -> 'b) -> ('c -> 'a) -> ('c -> 'b)
.) This could work for dimensions that are unknown at runtime for Haskell or OCaml as their polymorphic functions can be implemented by a single machine code function where C++ templates / Rust generics must monomorphize (generate different machine code functions for different types). You would probably want existential types (though OCaml and Haskell have them).
I think the problems are more things like:
- that type only works on matrices, you can’t so easily express that eg * in APL works on two scalars, or two vectors of the same length, or a matrix and a rank-3 array so long as their dimensions line up appropriately.
- handling operations that change lengths is hard: concat probably wants you to be able to unify through certain arithmetical expressions, and the filter operation (take an vector and a bitvector the same length, and produce the vector of elements where the bit was set) means you probably want a natural way to handle those kinds of existential types for lengths: you get a vector, and it has a length, but you’re not sure what it is.