Fork me on GitHub

Do not let your type system reason about aliasing in your programming language

Posted on September 22, 2026

This post is a followup to the one about the plans for version 1.0, and is based on my experience trying to address one of the outstanding issues that I had described as “easy to fix”. As I will discuss below, it’s basically a typo that is easy enough to fix, but doing so breaks code in ways that raise nontrivial design questions, and further pulling on the thread made me discover a related issue, the solution to which has made me rethink some of Futhark’s oldest design choices. In this post I will explain which unusual type system feature causes all this trouble (it’s basically aliasing, but not in the way you may know about from discussions about aliasing in C), why it is not so easy to fix, and which options we are considering. The bottom line is: unless you have a good reason to pick this fight, don’t do it. The explosion in complexity is not trivial.

Background

Perhaps Futhark’s most unusual type system feature is in-place updates - it is a feature that lets us write expressions such as

A with [i] = v

to obtain a semantic copy of the array A with the element at index i replaced by v, but with the cost model guarantee that the cost is proportional to a single element, rather than the entire array A. The obvious implementation is to simply perform a destructive write to the memory where A is stored. To ensure this write cannot ever be observed, the type checker must ensure that the old value of A is never used on any execution path following the update. We say that A is consumed. In fact, we can largely ignore the fact that consumption is about in-place updates, and just treat it as an operation that makes the old value invalid somehow (maybe it becomes toxic!). This means that our correctness rule is something like this: objects have identity, and once an object is consumed, it may never be referenced again. In this perspective, a consuming operation like an in-place update semantically returns an object with a new identity, even though our operational goal is of course to reuse memory. The real challenge is that we want to statically ensure that this correctness rule is never broken at run-time, and hence we have to reason about identity in the type checker.

Specifically, when a variable A is consumed, we must also consume any variables that potentially have the same identity (operationally, “share memory”) as A, which we call the aliases of A. As an example, after the binding let B = A then B and A are aliased with each other. We can imagine that this is tracked by associating each variable with a set of its aliases. We then augment the type rules for every language construct to describe how the aliases of the result are constructed from the aliases of the constituent expressions. I will not go through all of them, but for example the result of an expression A unsurprisingly has the alias set {A}, and the array literal [x, ..., z] has an empty alias set, to indicate that it constructs a fresh array into which the elements are copied.

Conditional expressions are interesting, as the tracking of aliases is conservative, meaning that after a binding

let C = if ... then A else B

then we consider C to alias both A and B (and the other way), even though at run-time only one of these will actually be the case. This conservatism is key, because while rejecting a program at compile-time can be annoying, allowing a program to use a consumed value would be disastrous.

While the basic idea is easy enough to understand, a lot of complexity arises from the interaction with other language features, as well as some of our design constraints. While soundness (in the safety sense) is of course a fundamental requirement, the second-most important is perhaps simplicity. In-place updates are critical for certain algorithms (and can be used for cool hacks), but many programs do not use them at all, and should not be littered with more complicated syntax or rules than absolutely necessary. We try as hard as we can to enable programmers to pretend that this feature does not exist at all, whenever they do not need it. This is not easy at all. We also want all our rules for consumption and aliases to be local, meaning they require no costly whole-program analysis to check.

Functions

The most interesting feature in any language is functions. If we want a function f to be able to consume one of its parameters, we must make it clear to callers of f that the corresponding argument is consumed when calling f. We do this by essentially putting an effect (as in effect systems) on the function. A function is either consuming, written *a -> b, or observing, written a -> b. As a poorly conceived pun, we call this the diet of the function. When we apply a consuming function f to an argument A, then A is consumed, exactly as if it was the target of an in-place update. Since Futhark is a curried language, where a “multi-parameter” function is just a function that returns a function, this generalises nicely. For example, this function type consumes its second argument, but not its first:

a -> *b -> c

Another question is determining the aliases of a function. A reasonable rule seems to be that the result of a function application aliases all of its non-consumed arguments. But this makes aliasing quite promiscuous, meaning that quite soon everything aliases everything else, and it is also excessively conservative: most functions actually produce freshly constructed values. So we also allow a function return type to indicate the freshness of the result: either fresh (no aliases) or nonfresh (aliases all arguments). Slightly confusingly, this is also indicated with an asterisk:

a -> *b -- fresh result
a -> b -- nonfresh result

These asterisks mean something completely different from asterisks on parameters. In the return type, they describe the aliases of the result, while on parameters they denote a consumption effect. The similar notation is a relic of how this bit of language design evolved from Clean’s uniqueness types, which use an asterisk to denote uniqueness (but note that Futhark’s consumption/in-place feature is today completely unrelated to uniqueness types). There is a greater similarity with affine types, although they are still not the same thing. Futhark’s type system is more like an effect system that forbids a particular ordering of effects (consumption of a value followed by observing the value), along with a type system for propagating aliases.

Freshness and consumption annotations also impose constraints on function definitions. Consider this function definition:

def invalid (x: []i32) : *[]i32 = x

We declare that this function returns a fresh result, yet the result x aliases a non-consumed parameter. This is rejected by the type checker.

A somewhat more subtle rule is that even when a function is declared to return a nonfresh result, it may not return an alias to a global variable:

def global : []i32 = [1,2,3]
def f1 (b: bool) : []i32 = if b then global else [4,5,6]

Consider an application f1 true. What should be the aliases of the result? Nowhere in the type of f1 does it mention global, so there is no way we can infer this alias at the application site. For this reason, we forbid f1 at its definition site, according to this rule:

An alternative solution would be to augment our type system with a more precise notion of aliasing. This would allow f1 to specify that the result may alias global, and it could also allow other functions to more precisely specify the aliasing relationships between results and parameters. We do not do this for the sake of simplicity: Futhark is not a language for reasoning carefully about lifetimes or aliases, the way for example Rust is. The only reason we go to all this effort is to allow the expression of certain algorithms that need performance guarantees only reachable through in-place updates, and we want as small a language feature as possible that still satisfies this requirement.

Another edge case is what it means for a tuple (or record) result to be fresh. Consider this definition:

def f2 (n: i64) : *([]i64, []i64) =
  let arr = iota n
  in (arr, arr)

Here, iota is the usual function that constructs a fresh index array of size n. While arr itself has no aliases, and hence the result of f2 does not alias a parameter or global variable, this is still a problematic definition. Consider this binding:

let (a,b) = f2 n

Since we know that f2 returns two arrays that are the same, a and b share memory and hence are conceptually aliased, but this does not appear anywhere in the type of f2. We therefore add this rule:

This is checked at the definition site of f2, and the function above is therefore rejected.

Here I should note that in Futhark’s alias system, only arrays and abstract types (because they might be arrays) carry aliases on their own. Primitive types such as i64 have “value semantics” in the sense that any use involves a copy, and tuples, records, and sum types are just thin frames around their components. This means that a return type *([]i64, []i64), as in f2, is actually interpreted as (*[]i64, *[]i64).

Higher-order functions

Higher-order functions do add some complexity to the problem, but they are not so difficult as long as we are dealing only with concrete types.

Consider the following higher-order function:

def f3 (p: bool -> []i32) =
  let x = p true
  let y = p false
  in ...

We apply the function p to some arguments and get back arrays x and y. Are we allowed to consume them? By the reasoning above, it seems the answer is yes: since p returns a nonfresh result, x and y alias the arguments to p, which are just booleans, and since primitive values do not carry aliases, this seems fine. However, note that p does not return a fresh array - this means an application of f3 could be something like this:

let arr = [1,2,3]
in f3 (\b -> arr)

Now every time we apply p inside f3 we get a reference to arr. Clearly consuming it is disastrous. How should we resolve this? One solution is to impose the same constraint on anonymous functions as on top level functions, which is that they must not return an alias to a free variable. Then the above would be a type error, and we would have to write this instead:

let arr = [1,2,3]
in f3 (\b -> copy arr)

The copy function accepts a value and returns a fresh one (at a cost), and is a useful workaround for many alias-related errors. In practice, this approach leads to intolerable amounts of boilerplate, as well as the overhead of copy. Our solution has two parts:

  1. Local functions such as lambdas are allowed to return aliases to (non-global) variables in scope.

  2. We change our aliasing rules for function applications such that the aliases of the function itself are also applied to the result of the function application.

In the definition of f3, this means that the arrays x and y alias the function parameter p, and since p is not consumable, neither are x and y. The operational interpretation is fairly straightforward: functions contain a closure, and the result of a function application may alias that closure.

For top level functions, we require that the result may not alias the closure (that is what the “may not alias free variables” rule really says). We could have used the same rules for both cases, or flipped them for that matter, without losing soundness, but we have found the inconsistency to result in better ergonomics. For example, consider the top level transpose function:

val transpose [n][m] 't : [n][m]t -> [m][n]t

It would be quite annoying if an application transpose X would alias transpose itself, since that means we would not be able to consume the result (as that might consume transpose multiple times). For this reason we impose stricter rules on top level functions. Expressed in terms of aliasing, we pretend that top level functions are defined in an empty environment, meaning their closure alias is the empty set, as our aliasing restriction on their definition means that the result cannot alias anything in the environment.

(Some readers of a particular functional bent may now be thinking: hang on, does parametricity not tell us that the result of transpose cannot possibly alias anything but its argument? It does, and we will see how we might exploit parametricity in a bit.)

Polymorphic and abstract types

Futhark has a fairly standard system of parametric polymorphism, and the restrictions related to first class functions do not matter for aliasing. The basic principle is pretty simple: since every type parameter might be instantiated as an array, we need to carry aliases for every variable of an abstract type, and essentially treat them as if they were arrays. For ordinary type parameters this largely just works out without any great surprises, but it has some consequences for doing generic programming with abstract types using Futhark’s module system.

In Futhark, when you define a module, you match against a module type that specifies the behaviour of the module in an abstract way. A module type is essentially a sequence of type and value specifications, but with no definitions. We might imagine a module type MT0 for numbers that looks like this:

module type MT0 = {
  type t
  val zero : t
  val one : t
  val plus : t -> t -> t
  ... -- various other useful operations
}

This states that there is some abstract type t, of which nothing is known, and various functions that can operate on t, and in this case also two constants of type t. The specification above is quite similar to what you will find in Futhark’s prelude, except that the prelude defines a hierarchy of module types, and of course contains many more operations. The nice thing about the module system is that we can write generic code (parameterised modules) against the interface itself, which can then be instantiated with any concrete implementation of the module type.

Since the type t is fully abstract, it can also be an array, and so must be treated conservatively, including alias tracking, even though the module type may not provide any function that actually consumes a t. This turns out to have a rather major ergonomic consequence. Suppose we have a module M0 that implements the module type MT0:

module M0 : MT0 = {
  -- Definition does not matter
  ...
}

We then define this function:

def add_one (x: M0.t) : M0.t = M0.plus x M0.one

This turns out to be forbidden! The reason is a bit subtle, but explainable in terms of the rules discussed previously. If we look at the type of M0.plus above, we see it returns a nonfresh result, and hence the result of M0.plus x M0.one aliases both arguments. The alias of x is fine, but the alias to M0.one is not good, because M0.one is a global variable, and functions are not allowed to return aliases to global variables. It took us a while to discover this problem, for the rather embarrassing reason that we had a typo in the type checker that made it ignore the aliases of global variables of abstract type, and even after noticing this bug, we did not fix it because it had consequences for the language ergonomics that we wanted to consider carefully first. Suppose we fix the bug in the type checker, which is very easy. Now functions like add_one become a type error, and it turns out they are very common in module-generic Futhark code. Let us consider how to fix them.

One easy fix is to add an explicit copy to add_one:

def add_one (x: M0.t) : M0.t = copy (M0.plus x M0.one)

But this is boilerplate at best, or inefficient at worst. The more principled solution is to modify the module type specification such that plus produces a fresh result:

val plus : t -> t -> *t

The downside is that this adds clutter to interfaces. It turns out that most functions conceptually produce fresh results, and so they should all have this asterisk in order to avoid overly promiscuous aliasing in callers. This is in violation of our hope that Futhark programmers can ignore the entire consumption/aliasing system when they do not need it, since now it does turn up in the types of fundamental functions.

This has made us consider whether the default should be flipped, such that by default a function a -> b is assumed to return a fresh result, and you need an annotation to indicate nonfreshness. E.g. we might say that the type of transpose should be written like this:

val transpose [n][m] 't : [n][m]t -> @[n][m]t

The @ symbol could of course be something else; the point is that it is arbitrary whether we require extra syntax to mark freshness or extra syntax to mark nonfreshness. But no matter what, programmers will not be able to be completely ignorant of this facet of the type system.

But ergonomics are not the only issue

Abstract types turn out to be the major source of trouble here. It is not terribly surprising in retrospect, since abstraction is all about hiding information. Let us return to the example with “self-aliasing”:

def f2 (n: i64) : *([]i64, []i64) =
  let arr = iota n
  in (arr, arr)

This function is disallowed because we claim to produce a fresh result, yet components of the result alias each other.

Now consider this module interface:

module type MT1 = {
  type obj
  val mk : bool -> obj
  val consume : *obj -> *obj
}

This interface says there is an abstract type obj, a way to construct obj (but nonfresh ones), and a way to consume obj. Now consider this implementation M1 of the module type MT1:

module M1 : MT1 = {
  type obj = ([1]bool, [1]bool)
  def mk (b: bool) : obj = let arr = [b]
                           in (arr, arr)
  def consume ((x,y) : *obj) : *obj = (x with [0] = true,
                                       y)
}

On its own, this module is fine:

But now let us consider a use of the module M1:

let foo = M1.mk true
let bar = M1.consume foo

This is well-typed. M1.mk produces a nonfresh obj that aliases true (i.e., the empty set), which we can freely pass to M1.consume. But if we peek across the abstraction, things look bad, because foo is a pair of arrays that alias each other, so when we do an in-place update on x in M1.consume, we also modify y. This is very bad, and the problem is that by hiding the fact that M1.obj is a tuple, we make it impossible to track that foo contains self-aliasing.

This is difficult to fix due to how Futhark’s module system (which is really a module language) works. Defining a module and matching it against a module type are distinct operations, and for that matter a module is often matched against multiple module types. This is a big strength of the module system (for reasons outside the scope of this post), but it means we cannot just invent a rule that bans the definition of M1.mk. It might be possible to modify the module system such that the module M1 no longer matches the module type MT1, justified by freshness and potential self-aliasing, but that complicates the module system, which seems a bad tradeoff.

Instead, our solution is to augment the notion of an alias set. It is no longer just a set of names, but may also include a distinct self element that denotes “potential self-aliasing”. We then add a rule:

This is very similar to the rule banning consumption of global variables, and can in some sense be seen as an implicit global variable.

We then add another wrinkle to the aliasing rule for function applications:

This means that the application of M1.mk works, but the application of M1.consume now fails. This can then be fixed with a copy, but the best solution is to modify the specified type of mk to return a fresh result (as is logical for a “constructor function”). A type system must remain sound even for code that is not written according to what we consider best practice.

Back to ergonomics

Many times during development, I thought we had finally fixed the last minor issue with the type system. Alas. At this point I think all soundness issues have been addressed, and I even started working on a mechanised formalisation in Rocq to make sure of it this time, although it’s not done yet. However, the last fix added an ergonomic issue. Consider the identity function:

val id 'a : a -> a

The return type of id is nonfresh, because it returns its argument without copying it.

Now assume we have some value x of some abstract type t but which is not self-aliased. If we then do an application

let y = id x

then y is suddenly self-aliased. This is because the concrete instantiation of id has type t -> t, meaning we are applying a function that returns a nonfresh result of abstract type t. According to the rule above, we then inject the self element into the alias set of the result. This is not unsound, but it means all routine convenience functions like id, pipelining, function composition, etc. are now lossy in terms of aliasing. This often results in spurious and annoying aliasing errors; the kind where you end up frustrated with the idiotic type checker that rejects obviously sensible programs.

Again, a solution would be to have a richer type language, perhaps similar to Rust, where we could directly describe the potential aliases of id. We might imagine we could give id this type scheme:

val id 'a : (x: a) -> a @ {x}

This hypothetical notation states that id accepts a parameter named x, and the aliases of the result are (at most) the set {x}. But I really do not want to extend the fundamental type system (in particular the language of types), because it has major implications everywhere, and aliasing/consumption is meant to be a niche feature.

Instead, I am playing around with a solution that exploits parametricity to locally infer more precise aliasing without having to extend the language of types itself. Parametricity is a concept from programming language theory that says that all instantiations of a parametrically polymorphic function “behave the same way”. Operationally, we can think of it as polymorphic functions not being able to “reflect” on their instantiation type. By exploiting parametricity, we can infer various properties of a function solely by its polymorphic type, as discussed in the famous paper Theorems for free!.

Consider again the type of id:

val id 'a : a -> a

It is clear that the only way this function can return an a is by returning the a we give it, since it knows nothing about it. (It can also crash, of course.) By this we can infer that the aliases of the result can at most (actually exactly) be that of the argument.

Now consider the function apply, which applies a function to an argument:

val apply 'a 'b : (a -> b) -> a -> b

While apply is hardly a very useful function, its type is isomorphic to that of the very common pipelining operators |> and <|.

The only way apply can return a b is to get a b from the function. This means we can infer that the aliases of an application apply f x must be the same as the aliases of any possible application of f to any arguments of appropriate type, which in this case is x and f itself. While Futhark’s notation for types is not rich enough to let us write this information directly, it seems like it can be inferred to an extent that is sufficient to provide ergonomic alias analysis of common utility functions.

Parametricity can only take us so far, of course. Consider a contrived function that takes a function and two arguments of the same type and returns a pair of the two applications:

val apply2 'a 'b : (a -> b) -> a -> a -> (b,b)

Parametricity does not let us infer that the two results do not alias each other, because it is possible to define apply2 such that they do.

I am still playing around with exactly how far to push this notion of parametricity, and the book-keeping becomes slightly intricate. I definitely want id x (and similar) to be possible without loss of aliasing fidelity, but perhaps it is fine to require a distinct apply for the case where the result is fresh, which turns out to be the important special case in practice:

val apply_fresh 'a 'b : (a -> *b) -> a -> *b

For the pipelining operators, we might spell that as:

val (|>*) 'a 'b : a -> (a -> *b) -> *b

It means many higher-order operators and functions would exist in a “fresh” and “nonfresh” variant. This is tolerable (and sound), but less convenient, so I hope we can come up with a system where this is not necessary.

From a research perspective, I find this application of parametricity quite interesting. I have always found the idea of free theorems to be more of an intellectual curiosity (as I am not much of a PL theorist), and using it as a building block in a real type system is very alluring.

What we will do

What do we make of all this? I am not sure yet. We must come up with some form of resolution to the soundness issues before releasing 1.0, and it is guaranteed that some code will break. That is why I want it to be done by the time we release 1.0, as I want that version number to signal some kind of stability. So far I am leaning this way:

I feel that I am fiddling with such conceptually explosive parts that I need to discuss the design with other people. The soundness issues I can resolve on my own, but the design space is vast with respect to what makes for an ergonomic programming experience. If anyone has an opinion, feel free to come by my office, nail your ideas to a church door, or perhaps more practically send me an email, write me on IRC, or let your voice be heard on social media.

That said, while I intend to see this fight through to the end, I strongly recommend that other language designers enjoy this battle from afar. This is not a feature I suggest adopting for languages that do not have very particular performance requirements. In particular, most languages that want in-place updates should probably just use APL/SaC/Koka/Lean-style reference counting, which reuses memory when the count is one and copies otherwise, but in Futhark we have operational needs where we must guarantee that no allocation takes place.