Towards Hybrid Array Types in SAC

Array programming is characterised by a formal calculus of (regular, dense) multidimensional arrays that defines the relationships between structural properties like rank and shape as well as data set sizes. Operations in the array calculus often impose certain constraints on the relationships of values or structural properties of argument arrays and guarantee certain relationships of values or structural properties of argument and result arrays. However, in all existing array programming languages these relationships are rather implicit and are neither used for static correctness guarantees nor for compiler optimisations.
We propose hybrid array types to make implicit relationships between array values, both value-wise and structural, explicit. We exploit the dual nature of such relations, being requirements as well as evidence at the same time, to insert them either way into intermediate code. Aggressive partial evaluation, code optimisation and auxiliary transformations are used to prove as many explicit constraints as possible at compile time. In particular in the presence of separate compilation, however, it is unrealistic to prove all constraints. To avoid the pitfall of dependent types, where it may be hard to have any program accepted by the type system, we use hybrid types and compile unverified constraints to dynamic checks.