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

# Do not let your type system reason about aliasing in your programming language Source: [https://futhark-lang.org/blog/2026-09-22-aliasing.html](https://futhark-lang.org/blog/2026-09-22-aliasing.html) Posted on September 22, 2026 This post is a followup to[the one about the plans for version 1\.0](https://futhark-lang.org/blog/2026-08-26-towards-1.0.html), and is based on my experience trying to address[one of the outstanding issues](https://github.com/diku-dk/futhark/issues/1675)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](https://github.com/diku-dk/futhark/issues/2531), 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](https://futhark-lang.org/blog/2026-09-22-aliasing.html#background) Perhaps Futhark’s most unusual type system feature is[in\-place updates](https://futhark-lang.org/blog/2022-06-13-uniqueness-types.html)\- it is a feature that lets us write expressions such as to obtain a semantic copy of the array`A`with the element at index`i`replaced by`v`, but with the[cost model guarantee](https://futhark-lang.org/blog/2022-01-27-cost-models-are-contracts.html)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 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](https://futhark-lang.org/blog/2024-04-18-random-numbers-with-uniqueness-types.html)\), 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](https://futhark-lang.org/blog/2026-09-22-aliasing.html#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: 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](https://clean.cs.ru.nl/download/html_report/CleanRep.2.2_11.htm), 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](https://users.cs.northwestern.edu/~jesse/pubs/alms/tovpucella-alms.pdf), 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: - 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\. ### [Tuples](https://futhark-lang.org/blog/2026-09-22-aliasing.html#tuples) 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: 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: - 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](https://futhark-lang.org/blog/2021-08-02-value-representation.html)\. 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](https://futhark-lang.org/blog/2026-03-04-array-record-updates.html), 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](https://github.com/diku-dk/futhark/issues/2456), but it is too incomplete to be worth getting into\. ### [Higher\-order functions](https://futhark-lang.org/blog/2026-09-22-aliasing.html#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 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: 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`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]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](https://www.cl.cam.ac.uk/teaching/1617/L28/parametricity.pdf)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](https://futhark-lang.org/blog/2026-09-22-aliasing.html#polymorphic-and-abstract-types) Futhark has a fairly standard system of parametric polymorphism, and the[restrictions related to first class functions](https://futhark.readthedocs.io/en/latest/language-reference.html#higher-order-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](https://futhark-lang.org/blog/2017-01-25-futhark-module-system.html)\. 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](https://futhark-lang.org/docs/prelude/doc/prelude/math.html), 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](https://futhark-book.readthedocs.io/en/latest/modules.html#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](https://github.com/diku-dk/futhark/blob/8b23e0085bbbafb1f9685bc57626627d4a0ee2e5/src/Language/Futhark/TypeChecker/Consumption.hs#L398), 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: 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](https://futhark-lang.org/blog/2026-09-22-aliasing.html#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: - The`obj`type is a pair of single\-element arrays of booleans\. - The`mk`function returns a tuple with self\-aliasing, but since it claims to return a nonfresh result, that is allowed\. - The`consume`function has a consuming parameter of type`obj`, and consumes one of its components\. It is in fact very similar to function`f3`that we saw before\. 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*\. 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\. ### [Back to ergonomics](https://futhark-lang.org/blog/2026-09-22-aliasing.html#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: 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 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\!](https://dl.acm.org/doi/10.1145/99370.99404)\. Consider again the type of`id`: 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](https://futhark-lang.org/blog/2026-09-22-aliasing.html#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: - 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](https://hjemmesider.diku.dk/~athas/#where),[nail your ideas to a church door](https://en.wikipedia.org/wiki/Ninety-five_Theses), 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](https://sac-home.org/)/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\.