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.
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] = vto 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 an alias set, which a
set of the variables it 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 Bthen 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.
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 -> cAnother 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 resultThese 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 = xWe 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:
- A top level function definition may not return a value that aliases anything but the function parameters.
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 question 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 nSince 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:
- When returning a tuple that is declared fresh, every component must be fresh, in the sense that none of them alias each other.
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).
There’s a few more wrinkles to go. If a function returns a nonfresh pair, like the one with this type:
bool -> ([]i64, []i64)Then there is a possibility that the two arrays alias each other, just as with
f2 above. Hence we add another alias propagation rule to function application:
- If a function returns a tuple, then all of its nonfresh components alias each other.
There is also a problem on the consumption side. Consider this function, which has a consuming parameter that happens to be a tuple:
def f3 [n] ((x,y): *([n]i32, [n]i32)) =
let x' = x with [0] = 0
in (x', y)First, for this to be valid in an intuitive sense, we need a guarantee that the
two components of the xy tuple do not alias each other. This requires a rule
in function application:
- When passing an argument for a consuming parameter, the tuple (or record) components may not alias each other.
Note that in f3, the tuple is immediately destructured through pattern
matching, before it ever gets a name. Consider what would happen if we wrote it
like this instead, using projection to extract the tuple components:
def f3_bad [n] (xy: *([n]i32, [n]i32)) =
let x = xy.0
let y = xy.1
let x' = x with [0] = 0
in (x', y)This function fails in current Futhark, as both x and y alias all of xy
(or rather, both components of xy), and hence the update to x also consumes
xy, which makes the later reference to y invalid. This is arguably a design
flaw that we currently paper over with syntactic
sugar, but which I would like to fix in a
better way.
I suspect the handling of tuples can be improved by refining our alias sets to no longer be sets of variable names, but variable names along with a position, which allows us to alias only part of a tuple. If we then consume a tuple component, then the tuple as a whole can no longer be referenced, but other unconsumed subcomponents can still be used. I did already do some exploratory work in this regard, but it is too incomplete to be worth getting into.
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 f4 (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 f4 could be something like this:
let arr = [1,2,3]
in f4 (\b -> arr)Now every time we apply p inside f4 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 f4 (\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:
- Local functions such as lambdas are allowed to return aliases to (non-global) variables in scope.
- 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 f4, 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]tIt 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.)
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.oneThis 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 -> *tThe 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]tThe @ 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.
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:
- The - objtype is a pair of single-element arrays of booleans.
- The - mkfunction returns a tuple with self-aliasing, but since it claims to return a nonfresh result, that is allowed.
- The - consumefunction has a consuming parameter of type- obj, and consumes one of its components. It is in fact very similar to function- f3that we saw before.
But now let us consider a use of the module M1:
let foo = M1.mk true
let bar = M1.consume fooThis 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. 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. Therefore we cannot enforce the rule that an argument passed for
a consuming parameter may not have components that alias each other.
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:
- A program may not consume an alias set containing the self element.
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:
- If a function returns a nonfresh value of abstract type, then that value aliases the self element.
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.
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 -> aThe 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 xthen 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 -> aIt 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 -> bWhile 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 -> *bFor the pipelining operators, we might spell that as:
val (|>*) 'a 'b : a -> (a -> *b) -> *bIt 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 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:
- Keep the notation where - *denotes freshness and the absence denotes nonfreshness. Perhaps we will rename “nonfresh” to “stale”, although I feel this term sounds unnecessarily negative. Flipping the default would change over ten years of convention, so I would need very strong evidence that it is better. This means we will need to add- *to most return types in the prelude, and just teach people what they mean, or to ignore them.
- Fix the soundness issues, in particular by adding the notion of the self element.
- Keep the type and module language unchanged.
- Use parametricity to infer more precise aliases for polymorphic functions. This is reasonably easy to do for first-order functions, and I hope we can also do a good job with higher-order functions.
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.