Why You Shouldn't Put Aliasing in Your Type System
The Futhark team is days from shipping version 1.0, and the one issue they labeled "easy to fix" turned out to be a typo in the type checker whose correction br...
One Asterisk, Two Meanings
The Futhark team is days from shipping version 1.0, and the one issue they labeled "easy to fix" turned out to be a typo in the type checker whose correction breaks real, working code. Fixing it forces a design decision that touches Futhark's oldest and most unusual feature: in-place updates backed by an aliasing system that the type checker verifies. The author's verdict on all of it is blunt: "unless you have a good reason to pick this fight, don't do it. The explosion in complexity is not trivial."
In-place updates are Futhark's performance wedge. The expression
A with [i] = v
semantically returns a copy of A with one element replaced, but the cost model guarantees the operation is O(1), proportional to a single element. The obvious implementation is a destructive write to A's memory. The type checker's job is proving that write is never observable: the old value of A must never be referenced on any execution path after the update. Futhark calls this consumption — the variable is consumed, and everything that shares its identity, its aliases, is consumed with it.
The rules track an alias set per variable. let B = A makes B and A alias each other; a fresh array literal has an empty alias set. A conditional is conservative: let C = if ... then A else B makes C alias both A and B, even though at runtime only one branch executes. This conservatism is deliberate. Rejecting a program at compile time is annoying; silently letting a consumed value escape is a correctness disaster, and for a language whose entire pitch is predictable performance, soundness beats convenience.
Functions complicate the picture. A function that may consume one of its parameters must say so, which Futhark does by tagging the parameter type with an asterisk — a consuming (*a -> b) versus an observing (a -> b) "diet". The same asterisk on a return type means something completely different: a fresh result (a -> *b) carries no aliases, while a nonfresh result aliases all non-consumed arguments. One symbol, two meanings, a relic of Clean's uniqueness types. The result of transpose X aliases X unless transpose promises freshness.
Three design constraints shape every rule: soundness, locality (no whole-program analysis; each call site must be checkable in isolation), and a near-religious commitment to simplicity. Most Futhark programs never use in-place updates and should not pay for them. The global-variable rule is a taste of that tension: a top-level function may not return a value that aliases anything but its parameters, because there is no slot in the return type to advertise "this result aliases global". Futhark explicitly refuses the richer alias-language Rust would use: "Futhark is not a language for reasoning carefully about lifetimes or aliases."
Tuples and Higher-Order Functions: Where "Fresh" Leaks
Arrays and abstract types are the only values that carry aliases. Primitives have value semantics; tuples are thin frames. This choice quietly drives the rules. A "fresh" tuple result means every component is fresh: none may alias another. So let arr = iota n in (arr, arr) cannot be a *([]i64, []i64) result — arr self-aliases.
The consumption side is subtler. A consuming tuple parameter requires that the components do not alias each other. Pattern-match destructuring gets this for free; projection (xy.0) does not. Consume one projected component and the whole tuple is consumed with it. Futhark papers this over with syntactic sugar today, but it is a known flaw: the author wants aliasing to be tracked per position inside a tuple, not as a whole.
Higher-order functions are tractable for concrete types, but capture breaks it. If p returns nonfresh arrays and f4 applies p twice, x and y alias p's arguments. If p is a lambda that closes over a local arr, consuming the result mutates arr — "disastrous". Banning lambdas from returning aliases of free variables forces copy arr boilerplate everywhere. Futhark's compromise has two parts:
- Lambdas may return aliases of non-global variables in scope.
- The aliases of the function itself (its closure) are applied to the result of the application.
Consequence: x and y in f4 alias the parameter p; p is not consumable, so neither are they. Top-level functions get a stricter rule — the result may not alias the closure — because top-level code is defined in an "empty environment". The inconsistency is deliberate: a transitive alias to transpose itself would make consuming its result useless. The author flags the parametricity reading here: transpose cannot alias anything but its argument, a free theorem the type system does not yet exploit.
The Abstract-Type Typo and the Self Element
Here is where the "easy to fix" issue actually lives. Futhark's module system gives you abstract types: type t with no structure, plus values like zero, one, plus : t -> t -> t. Because t might instantiate to an array, every value of an abstract type must carry alias tracking. The fallout is that a common, sensible function becomes a type error:
def add_one (x: M0.t) : M0.t = M0.plus x M0.one
M0.plus returns nonfresh, so its result aliases both arguments — including M0.one, a global. The no-global-alias rule rejects it. The cause: a typo in the type checker that ignored aliases of abstract-type globals. The fix is a one-liner in the checker; the consequence is that nearly every module-generic function suddenly needs an explicit copy (boilerplate, or a real allocation) or a fresh-marked interface:
val plus : t -> t -> *t
Now the asterisk — a performance feature that most code should be able to ignore — pollutes fundamental interface signatures. Futhark is weighing flipping the default: a -> b means fresh by default, with a new @ annotation for nonfresh. The symmetry cuts both ways; either choice keeps the system visible in the prelude. Ten years of convention weighs against flipping.
Abstraction also creates a soundness hole, not just ergonomics. An abstract obj may be implemented as a self-aliasing pair of arrays. mk returns it nonfresh, consume takes a consuming *obj. Both check fine locally. But if the implementation pairs two aliasing arrays, consuming one in-place silently mutates the other — and the module interface cannot express that. Futhark's fix introduces a self element in alias sets: "potential self-aliasing", treated like an implicit global. A nonfresh abstract-type result acquires the self element, and any program that would consume it is rejected. Soundness over elegance, as always in this design.
Parametricity as a Free Type Feature
The self element fixes soundness but creates a new ergonomic wound. The identity function is nonfresh — it returns its argument without copying. Pass a value of abstract type through id and it suddenly carries the self element, even when nothing is actually self-aliased. Now id, pipelining, and composition are all lossy alias analysis, and the type checker rejects "obviously sensible programs". The author's answer: exploit parametricity to infer precise aliases without extending the type language.
Wadler's "Theorems for free" says a parametrically polymorphic function cannot reflect on its instantiation — it treats a as an opaque box. From val id 'a : a -> a the only way to produce an a result is to return the a you were given. So the result's aliases are exactly the argument's. No self element, no loss. The same reasoning covers apply and the pipe operators: apply f x aliases f's closure plus x. Where parametricity stops paying off is equally instructive. A function apply2 that applies f to two a arguments and returns the pair (b, b) — parametricity cannot prove the two results do not alias; f is free to return the same array twice.
The design bet is this: a narrow, locally sound inference rule derived from the polymorphic type signature, leaving the surface syntax unchanged. Futhark's current draft plan: keep the asterisk notation (freshness marked, nonfreshness unmarked), add the self element, keep the module language intact, and infer parametric aliases for first-order polymorphic functions — with a apply_fresh / |>* variant where the result must be fresh, the case that matters in practice.
The Tradeoff Stack, and Why Most Languages Should Sit This Out
The Futhark case is a masterclass in what an aliasing discipline costs when it lives inside the type system rather than beside it:
- Syntax pollution: every prelude function may need
*on its result to avoid promiscuous aliasing in callers. - Implicit soundness rules: fresh tuple components, no global aliases, no component-self-aliasing in consuming parameters — none of which you can see in a function's declared type.
- Abstraction leakage: generic code over abstract types either pays allocation for
copyor must mark constructors fresh; the module system's single-definition/multiple-interface design makes local rules insufficient.
The operational target is what justifies it. Futhark's in-place update is not "reuse when cheap" — it is a hard no-allocation guarantee for performance-critical array code. That is a reference-counting regime: APL, SaC, Koka, and Lean-style systems reuse memory at count one and copy otherwise, which gives you the allocation option. Futhark demands the allocation absence, which is why the type checker must prove consumption sound rather than measure it at runtime.
The engineering lessons port to languages that do manage aliasing. In Rust, the borrow checker encodes the same conservative choice — reject at compile time over gamble at runtime — but Rust's lifetimes are visible in types, which is exactly what Futhark refuses to do. Go has no equivalent story: reflect, unsafe.Pointer, and escape analysis (a runtime-adjacent compiler inference, not a type-level contract) leave the aliasing question to the GC and the heap, at a predictable cost. If your workload can tolerate a copy, pick the copy; if it cannot, you inherit Futhark's problem, and this post is the map of that problem, including the parts they have not finished: per-position tuple aliasing, parametric alias inference for higher-order functions, and the open question of whether @ (nonfresh-by-exception) beats * (fresh-by-exception) as the default. Ten years of convention versus a cleaner interface — a decision with no cheap escape. That is what "easy to fix" actually costs.