okay i guess you're right since

   def cols [n] [m] 't (x: [n][m]t) : i64 = m

but that doesn't affect my point: cols has to know "something" about the name `replicate` more than just the types. why? because suppose i defined a function

   def replicate5 n x = replicate 5 x

then

   cols (replicate5 0 (replicate5 3 0)) == 5

that "something" is a shape function and now each data function must also correspond to a shape function. but that shape function doesn't magically have more info about its params than cols does about its params so you haven't solved any problem, you've just multiplied it.

spoiler alert every single tensor/array/matrix/ML/AI compiler runs into this same problem. there is only one solution: a fixed op set with a fixed number of corresponding shape functions. and then your compiler tries to perform shape inference/propagation. sometimes it works and you can specialize for fixed sizes and sometimes it fails and you get "dynamic" or "unknown" dims in your shapes and you can't do anything. oh well that's life in a universe where the halting problem exists.