The biggest semantic mess in Futhark

Summary

Posted on September 26, 2025 The original idea behind Futhark was that parallel programming (of certain problems) does not require a complicated language. Indeed, we believed that there was little need for the complexity to exceed that of the functional languages commonly taught to first year students at universities. (The complexity of parallel algorithms is another matter.) Overall, I think Futhark has succeeded at that. The meaning of a Futhark program is fairly easily determined using normal environment-based semantics; even tricky things like uniqueness types are mainly complicated in an operational sense, and to some extent in the type system - the meaning of a program (once it type checks) is obvious. This semantic simplicity is also evident in the implementation - while the compiler has lots of complicated optimisations and sophisticated transformations, the reference interpreter is largely straightforward, and quite similar in structure to how a person studying programming languages would write their first tree-walking interpreter. You will note that the above paragraph is full of words like overall, largely and fairly - this is because there is one language feature that has proven a particularly fertile ground for edge cases and implementation bugs. That feature is size types. In the following, I will explain why a seemingly simple type system feature has proven so surprisingly challenging. To recap the basic idea, size types allow Futhark functions to impose constraints on the sizes of their parameters. A simple example is a definition of the dot product, which takes two arguments that must be vectors of the same size: def dotprod [n] (x: [n]f64) (y: [n]f64) : f64 = f64.sum (map2 (*) x y) Here n is a size parameter that is implicitly instantiated whenever the function dotprod is applied, based on the concrete arrays it is passed. This by itself is not so difficult. Sizes can easily be incorporated into a type checking algorithm by treating them as types o...