Theories for data types have many important consequences for their effective use. Attempts to find a complete theory for arrays have raised as many questions as they have answered: the precise difference between nested and flat arrays, what empty dimensions mean computationally, whether arrays should be thought of as self-nested, and others. There appeared also to be many places where apparently free choices could be made that had a significant impact on the properties of the resulting type. We present a way of building theories of arrays (and other data types) based on category theory. The underlying mathematics gives complete theories in which the only choices are of the constructors used to form the type. It also gives a number of practi...
Add to ORKG