2011 | OriginalPaper | Chapter
Descriptor-Free Representation of Arrays with Dependent Types
Authors : Kai Trojahner, Clemens Grelck
Published in: Implementation and Application of Functional Languages
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 for bounds 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 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.