[etbebl]

OK seems interesting. Maybe what I actually want is fully dependent array types. But it seems like you should be able to do something like this:

  x : [{| col = #12 |}]float (* given *)

  x_split : [{| col = [| Top = #5, Center = #, Bottom = #5 |] |}]float = split_dim(x, "col", [| #5, #, #5|]) (* maybe type checking fails if the col dimension is not long enough?? *)

  x_center = \Phi i[{| col : # |}].x_split[{ col = Center i }]

Basically what I mean is, I can see benefits of declaring a sub-structure to a linear dimension using concatenations, rather than being limited to reshaping the dimension which only works if you can factor the length into N equal segments. Because many algorithms have to split a linear dimension in various ways and do something semantically different with the parts, and it would be cool to have the type system reflect and check this behavior. However, I think for it to be useful, it must be possible to "reinterpret" a dimension as having a particular structure (in a checked way), because if you're pipelining some array x through A and B, it's unreasonable to expect the author of A in every case to consider that you might want to apply B next and ensure that its output type permits that. And there are a lot of cases I can imagine where casting e.g. #m to [| #5, #n, #5 |] would only reasonably be considered a mistake, given the declared behavior of the function doing the casting, if m < 10.

Edit: maybe I'm silly in assuming you can't just downcast to a more specific shape type if you want to - still a newbie to algebraic typing.