Skip to main content

Size-Dependent Types for Practical Data-Parallel Programming

Martin Elsman ( University of Copenhagen )

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.

Speaker bio

Martin Elsman conducts research in the design and implementation of programming languages. Areas of research include compilation techniques for functional languages, in particular with focus on parallel languages, module systems, Web technology, program analyses for memory management, program optimisation, and domain-specific languages for financial contracts. Martin is Professor in the Programming Languages and Theory of Computation section at Department of Computer Science, University of Copenhagen (DIKU), where he serves as head of studies for a BSc degree in Computer Science and Economics. Martin is also an active maintainer of several software tools, including the MLKit, a full-blown Standard ML compiler, which targets both JavaScript and x86-64 machine code.




Share this: