This looks pretty compelling to me. I've been itching for a math-friendly language that makes it easy to work with arrays, vectors, vector spaces, manifolds, etc., but takes advantage of static typing. (Haskell is amazing but doesn't quite make linear algebra constructs feel native.)

On first read, it looks like this is designed with a healthy balance between mathematical insight (relationship of product types and tuples, basis in lambda calculus) and real developer needs (e.g., static typic is nice; dependently typed systems can be too much; types are great, but "nameless shapes" are useful, too).

I'd love to see an implementation of this to play around with.

Can't find a repo of this lang...

Is compelling to me because I'm in the hunt for marry array + relational (https://tablam.org)

This is great. For a long time I've had a gut feeling that there must exist a synthesis between pure functional, array, and data-oriented programming that gives you the best of all worlds:

Type safety, concise-to-the-point-of-terse code (with the types helping humans read it), and very high performance.

And this feels like a step in the right direction.

High-level array combinators seem to ignore memory locality performance details, to me. It's all fine to say you can arbitrarily reorder array indicies in a mathematical sense, but any real program that does that needs to change a lot of things. Similarly, using variant types to index into combined arrays, splits up underlying memory locality and adds "if" branches. Type systems that obscure these details will result is poorly performing code.

That said if you're going to do it, this seems like a reasonable set of primitives to do it with. I'm not a huge performance nut, so I'd love to give it a try.

I'd like to see an implementation in a language with only fixed-stride arrays. I'm not an expert, does Rust do this?

> we turn our attention to the dual of records – variants.

How is this the case, can someone give me an example?

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.