Size-Dependent Types for Practical Data-Parallel Programming

We present a type system for expressing size constraints on array types in an ML-style type system. The goal is to detect shape mismatches at compile-time without having to deal with all the consequences of a full dependent type system. The main restrictions are that the only terms that can occur in types are array sizes, which are constrained syntactically to be either variables or constants. For expressions that result in arrays of sizes that are not expressible using these restrictions, the system supports a form of existential types, with the type system automatically managing the requisite book-keeping, while guaranteeing that, at runtime, all arrays are regular. The type system forms the basis of the type system for Futhark, a data-parallel functional language (and compiler), which is aimed at generating efficient parallel code for GPUs and multi-threaded CPUs. Futhark is equipped with a number of first- and second-order array combinators, which have data-parallel semantics. Futhark performs a number of fusion, tiling and flattening transformations, and may even generate multiple code versions that are dispatched dynamically based on auto-tuned size-aspects of input data. The size-dependent type system works well with Futhark's support for higher-order modules and its limited form of higher-order functions, which are all eliminated entirely at compile time. We give examples of library functions and data structures that utilise the features of size-dependent types to express the intentions of how functions are used, for instance, to avoid out-of-bounds array-index errors and to guard against the composition of incompatible neural network layers. Futhark is joint work with a number of researchers at DIKU, including Troels Henriksen (DIKU), Cosmin E. Oancea, Ken Friis Larsen, Fritz Henglein, and Philip Munksgaard.