Descriptor-free representation of arrays with dependent types

Besides element type and values, a multidimensional array is characterized by the number of axes (rank) and their respective lengths (shape vector). Both properties are essential to do bound checking and to compute linear offsets into heap memory at run time. In order to have an array's rank and shape available at any time during program execution both are typically kept in an array descriptor that is maintained at run time in addition to the array itself.
In this paper, we propose a different approach: we treat array rank and shape as first-class citizens themselves. Firstly, we use dependent types to reflect structural properties of arrays in the type system. Secondly, we annotate a program with the array explicit array properties wherever necessary. This choice not only renders implicit run time array descriptors obsolete, but exposing all rank and shape computations explicitly in intermediate code also allows us to perform extensive compile time optimisation on them. We have implemented the proposed approach in our experimental array language Qube; preliminary experimental results indicate the suitability of the proposed approach.