An array-oriented language with static rank polymorphism
Justin Slepak, Olin Shivers, and Panagiotis Manolios.
ESOP, 2013 © Springer
Best Paper Award
The array-computational model pioneered by Iverson's languages APL and J offers a simple and expressive solution to the "von Neumann bottleneck." It includes a form of rank, or dimensional, polymorphism, which renders much of a program's control structure implicit by lifting base operators to higher-dimensional array structures. We present the first formal semantics for this model, along with the first static type system that captures the full power of the core language.
The formal dynamic semantics of our core language, Remora, illuminates several of the murkier corners of the model. This allows us to resolve some of the model's ad hoc elements in more general, regular ways. Among these, we can generalise the model from SIMD to MIMD computations, by extending the semantics to permit functions to be lifted to higher-dimensional arrays in the same way as their arguments.
Our static semantics, a dependent type system of carefully restricted
power, is capable of describing array computations whose dimensions
cannot be determined statically. The type-checking problem is
decidable and the type system is accompanied by the usual soundness
theorems. Our type system's principal contribution is that it serves
to extract the implicit control structure that provides so much of the
language's expressive power, making this structure explicitly apparent
at compile time.
PDF (448K) © Springer