- Descriptor-free representation of arrays with dependent types
- 20th International Symposium on the Implementation and Application of Functional Languages (IFL 2008), Hatfield, UK
- Book/source title
- 20th International Symposium on the Implementation and Application of Functional Languages (IFL 2008)
- Hatfield, UK: University of Hertfordshire, School of Computer Science
- Document type
- Conference contribution
- Faculty of Science (FNWI)
- Informatics Institute (IVI)
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.
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.