You raise some good points about the API readability and discoverability. For identifiers that the user is likely to write often, ASCII and standard naming conv

You raise some good points about the API readability and discoverability. For identifiers that the user is likely to write often, ASCII and standard naming conventions are usually preferable. While auto-completion is capable of handling unicode symbols, it can easily go overboard and harm usability. Agree that typealias could help, it's something we should explore. Thanks for the suggestions! Indeed you are correct about the finite dimension constraint, a problem we discussed with a recent reviewer [1] in further depth. As you correctly noted, since we have a fixed upper bound for type-level integers, when checking large tensors (i.e. whose width exceeds 1000 in any dimension), we fall back to dynamic shape checking, prior to numerical evaluation. Smaller tensors can be shape checked at compile time. I too, am wary of the "type voodoo" associated with type-level programming, but would argue that the added complexity from our approach (sans type level arithmetic) comes at very little cost to the end user due to type inference. In most cases we can check arrays at compile time. In the worst case, or if the user chooses, we use runtime shape checking or unsafe execution, which is the same as ordinary array programming. Thanks again for your feedback. Please don't hesitate to reach out if you have any further questions or comments! [1]: https://openreview.net/forum?id=SkluMSZ08H&noteId=BJeZ3FkuOr https://openreview.net/forum?id=SkluMSZ08H&noteId=BJeZ3FkuOr