Rewriting the Futhark type checker
The Futhark Programming Language
High-performance purely functional data-parallel array programming
Overview<br>Examples<br>Docs<br>Publications<br>Gotta Go Fast!<br>Get Involved<br>Blog
Fork me on GitHub
Rewriting the Futhark type checker
Posted on July 21, 2026
This post is about the evolution of Futhark’s type checker, motivated by a<br>large refactoring I am about to<br>merge. It is probably mostly of<br>interest to other language designers, and contains some lessons I wish I had<br>known when we first got started - although I am not particularly well-read in<br>the type checking literature, so it’s possible all of this is old hat.
Background
Far back in the primordial<br>era<br>when we first designed Futhark, the type system was simple: The only types were<br>scalars, arrays, and tuples, all functions were first-order and monomorphic, and<br>there was no type inference. All functions had to be annotated with their<br>parameter and return types. The only fancy feature that was present from the<br>(near) beginning was in-place updates via a kind of uniqueness<br>types, although at the time we didn’t really<br>understand how tricky they were.
At that<br>point<br>it really was just a type checker: starting from the facts that we were told<br>(the types of parameters), we checked if the types of expressions were<br>consistent, and tracked aliases to validate the use of in-place updates. The<br>implementation was a straightforward top-down single traversal of each function<br>in turn, during which AST were decorated nodes with their determined type, which<br>was then used by subsequent passes. It was the exact same kind of type checker<br>that I had been taught (and since taught myself) in a standard course on<br>programming language implementation, and when you can get away with it, this is<br>a good design: easy to implement, pretty efficient, easy to understand. At the<br>time we really didn’t understand the complexity of correctly checking the<br>rules for safe use of in-place updates, so the simplicity was perhaps illusory,<br>but we were happy in those days nonetheless.
Of course, we didn’t get away with it for long. We eventually started adding<br>features such as records and an<br>ML-style module system, and by version<br>0.4.0 we had put in higher-order functions and Hindley-Milner style type<br>inference. The implementation was a<br>classic (some might say “old-fashioned”) implementation of Algorithm<br>W;<br>the standard Hindley-Milner type inference algorithm. During traversal of a<br>function, we immediately solved type constraints. However, we had some type<br>system features that were never a natural fit with this approach. Both our<br>record system, and also our uniqueness types, depended on being able to query<br>the current type of some program fragment and make decisions based on it. This<br>would show up in cases like branches, where the aliases of if a then b else c<br>depended on whether the type of b and c can carry aliases (primitives<br>cannot). We managed to put together an implementation that worked by putting<br>various extra information into our representation of type variables, but it was<br>a little complicated, not obviously correct, and somewhat tedious to debug.
Later, when we added proper size types, we<br>did it by extending the basic Hindley-Milner system by essentially also treating<br>sizes as a kind of “type” subject to unification. At this point the system was<br>beginning to creak. Consider again a branch if a then b else c - what is the<br>size of the result? If b and c are arrays, we need to determine whether they<br>have the same size, and if not, generate an existential for the result size. But<br>at the point where we are looking at this if, we may not yet know whether they<br>are arrays! Many similar cases occurred, and the type system had various<br>restrictions and quirks where the well-typedness of a function would depend in<br>somewhat subtle ways on whether you had put in type annotations. One nice<br>property however was that if you put in type annotations on all parameters,<br>which is generally considered good style anyway, then things worked pretty<br>predictably. But still, the type checker was not particularly fun to hack on at<br>this point.
Eventually, this design - a single program traversal manipulating an<br>increasingly complicated state - stopped being workable. This was when we<br>started working on AUTOMAP, a (not yet finished)<br>system that loosely means that instead of saying map f x, you can just say f x and have the compiler figure out how many maps are needed. During this<br>work, we discovered that AUTOMAP had to work by taking a global view of a<br>function, typechecking it partially but without inferring specific sizes of<br>arrays, determining the smallest number of maps needed to make it typecheck<br>(by using an ILP solver), and then determine specific sizes. There was no way to<br>fit this design into the existing type checker, so I began taking it apart into<br>multiple phases.
The first phase I extracted was name<br>resolution.<br>It does what you would expect: resolves every name in the...