An array-oriented language with static rank polymorphism

Abstract

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. © 2014 Springer-Verlag.