[statusfailed]

Really nice! Had a quick read, here's my quick summary:

- Arrays are typed `S : D` with shape S and strides D

- Each of `S` and `D` is a nested tuple (instead of the flat tuples one typically sees in a tensor framework)

- Together `S` and `D` define the layout of a tensor

- Not every layout is "tractable", but the tractable ones form a nice category

A really good exposition, my only criticism is that it's quite front-heavy- it would be nice to see a detailed example like in 2.3.8 earlier in the document; there is a lot of detail presented early that doesn't seem necessary to understand the core ideas.

Last comment: I suspect there is a connection to strictification[0], would love to know more if the authors see this!

[0]: in the sense i mean here: https://arxiv.org/pdf/2201.11738v3