Posted on October 11, 2026
\nI recently wrote a post about open questions regarding alias propagation in the\nFuthark type checker. The questions have now been\nresolved, and while I am not going to re-explain the entire context for this\npost (it is by far the most complicated corner of the Futhark type system, in\nthe bad way), I want to summarise some of the most important design conclusions.\nSome of these deviate from what I normally consider good taste in language\ndesign, but they result in a design that is simple and supports the kind of\npatterns that appear in real Futhark code. I will also touch on why I have\nreasonable confidence that the design is sound, although only time will tell\nwhether it is also good.
\nThe basic problem is that in order to ensure safe use of in-place\nupdates, the Futhark type checker must track\nwhether two objects may potentially be aliased, meaning they share memory at\nrun time. Alias analysis has to be conservative, because while\nover-approximating the aliases of a variable, under-approximating can lead to\nunsoundness.
\nTo a large extent, alias analysis can be done using fairly intuitive rules\nstating how the aliases of an expression alias its subexpressions. The main\nchallenge is function calls. How can we know whether a function result aliases\nits input? In Futhark, this is part of the function type. A function with a\nreturn type of t indicates that the result may alias one of its parameters,\nwhile a function with a return type of *t indicates that the result is\nfresh, meaning it does not alias the parameters to the function. As an\nexample, this is the type of reverse, which returns a lazy “view” of the\ninput:
val reverse [n] 't : [n]t -> [n]tAnd this is the type of copy, which returns a fresh copy of the input:
val copy 't : t -> *tThis by itself is simple enough. The problem arises when we have polymorphic\nhigher order functions. Consider apply, the function that applies a given\nfunction to a given argument, which has this type:
val apply 'a 'b : (a -> b) -> a -> bSince apply must be applicable to all kinds of functions, both reverse and\ncopy, it cannot claim that the result is fresh. But intuitively, it is clear\nthat apply reverse x should alias x, while apply copy x should be fresh.\nYet since apply declares a non-fresh result, we seem forced to conservatively\ndeduce that the result aliases x. This is sound because it is an\nover-approximation, but it means that higher order functions have bad ergonomics\nwhen they interact with aliases. The function apply is of course a bit\ncontrived in this form, but it is exactly the type of the pipeline operator\n|>, which is commonly used in Futhark.
One way of fixing it would be to allow “freshness polymorphism” in the type\nsystem. We could imagine giving apply this type, where the result of apply\nis as fresh as the result of the function it is given:
val apply 'a 'b : (a -> F b) -> a -> F bThis would work, but also complicate the user-facing part of the type system.\nSince the only purpose of alias analysis is to secure a small part of the\nlanguage, I’d rather avoid complicating the type language.
\nHowever, the idea of having a more elaborate type system for reasoning about\n“freshness polymorphism” is a good idea; we just don’t want those types to ever\nappear in interfaces. The solution is to infer those more precise types, based\non the normal polymorphic types of Futhark functions, by exploiting\nparametricity. If we look at the type of apply, it is clear that the b\nthat is being returned can only come from the function - so we can infer that\nit must be as fresh as that function. Since b is a type parameter, the\nimplementation of apply cannot get a value of that type from anywhere else.
This perspective allows us to handle cases like apply reverse x and apply copy x precisely. The rule is that if a function result is a type parameter\nthat occurs only once in the result, and the only way to get a value of that\ntype is to apply a given function parameter, then the result inherits the\nfreshness of that function. For example, consider this higher-order function:
val apply2 'a 'b : (a -> b) -> (a -> b) -> a -> a -> (b, b)Here we cannot assume that apply2 copy copy x y has no aliases, because we do\nnot know whether apply internally applies only one of the functions and just\nreturns the same value twice. But now consider this more precise type:
val apply2 'a 'b 'c : (a -> b) -> (a -> c) -> a -> a -> (b, c)Now we do know, by parametricity, that these bs and cs can only come from\nthose function applications.
The idea is not so difficult, but I have agonised a lot over the implementation.\nSince this work is done as part of the road towards Futhark\n1.0, I very much want to avoid adding accidental\nunsoundness. For that reason, this type refinement is extremely conservative.\nSpecifically, it only kicks in for function applications where the function is a\npolymorphic variable, and the function has been fully applied to all of its\narguments. This basically means that refinement only takes place when you are\nnot doing tricks with partial application, and otherwise you get the “basic”\ninterpretation of the type, without taking advantage of parametricity. For\nexample, don’t do this:
\nlet foo = apply\nin foo copy xAnd don’t do this:
\nlet foo = apply copy\nin foo xOr rather, do it if you want, but you will get over-approximated aliases for the\nresults. The reason is that while handling the above is possible in a way that I\nthink is sound, it requires much more type-checking machinery, more\ncomplicated book-keeping, subtle side conditions, and results in inscrutable\ntype errors - and it mostly just supports code that does not look all that\nnatural. It rankles me to have basically syntactic constraints in a type system,\nbut since this does not affect the semantics of execution, but only refinement\nof certain types, I believe I can live with it.
\nThis part of the Futhark type system has been a perennial source of bugs, and we\nhave continuously underestimated how many edge cases would be encountered.\nPretty much every new feature has introduced unforeseen interactions. I was\nnaturally quite anxious about adding more flexibility. The most principled\nsolution is to formalise the system and prove it sound. I generally do not use\nmuch formal methods in my work, as I find that they add too much friction when\nresearching new optimisations and similar, but in this case we have a type\nsystem that is fairly stable (modulo the changes above), and we just want to\nknow that it actually works. While proving optimisations sound can be\nchallenging, proving soundness of type systems is not so bad, and as a PL\nresearcher, I do of course have some training in the area.
\nUnfortunately, “some training” does not go that far. While I can read and write\nformal definitions of dynamic and static semantics, understand judgments and the\nimplications of various soundness theorems, I was never particularly good at\nproving theorems, and I do not have the inclination or time to get better.\nFurther, nowadays a proof really ought to be mechanised, and I really do not\nhave the time or inclination to become a good Rocq or Lean user.
\nMany readers will probably be thinking about the elephant in the room: AI-driven\ncoding agents. My thoughts on these are complicated and to some extent still\nundecided, but this seemed like a case where they might serve. I could specify a\nsmall model language, including its dynamic and static semantics (“type rules”),\na soundness theorem for what must hold for well-typed programs, and have an\nagent construct a Rocq proof. I don’t have to understand how the proof works, as\nlong as I understand the theorem that it proves and the language and semantics\nthat it provies it for (which I do, because I defined them).
\nSo that is what I did. I will not go into detail on the formalisation, although\nit has some interesting parts, but it is basically a tiny subset of Futhark\nthat contains just three kinds of values: tuples, functions, and objects, with\nthe latter taking the same role as arrays in Futhark. The language has\nlet-binding, control flow, and creation and consumption of objects. The dynamic\nsemantics produce a “trace”, essentially a sequence of events, indicating when\nobjects (which have identity) are observed and consumed. A trace is good when\nan object is never observed after it is consumed. The correctness property is\nthat for a well-typed program, evaluating that program must always produce a\ngood trace. This property does not say anything about reusing memory, but it is\nclear that if a consumed object is never used again, the memory it resides in\ncan be reused.
\nI started out with a trivial language, and gradually extended it, eventually\nreached parametricity-based refinement of higher-order functions. Along the way,\nthe AI agent wrote and maintained the correctness proof, which in many cases\nalso involved adding additional preconditions to the type rules. In most cases,\nthese were mostly mechanical changes in order to make the proof go through, but\nthere were a few (somewhat uninteresting) tightenings of the type rules. One\ninteresting part of the experience is that I removed some features (such as\nrefinement through partial application) because they required semantic objects\nin the type rules that I felt were much too complicated.
\nThe implementation of alias propagation and checking in the Futhark compiler is\nnot directly based on the Rocq implementation. Rather, it is a reimplementation\nin Haskell based on the same algorithm and semantic objects. Futhark has a bunch\nof features that are not part of the Rocq proof (like sum types), and that is\ncertainly a place where errors can (and have) still sneak in, but I am now\nconfident that a sound system exists, and the question is just whether it is\nthe system we implemented in the compiler.
\nI am uncertain what to do about the formalisation. The proof itself is\ncompletely uninteresting - it is five thousand lines of machine-generated\nbrute-force proof-by-induction. My Rocq knowledge is not great, but it looks\nvery clumsy. I am fairly convinced it is not worth reading, and contains no\ngreat insights regarding proof techniques. It is only interesting as a\ncertificate that a desired property holds. Whether that type system is\ninteresting to others is again unclear. I obviously think it leads to a useful\nor pleasant programming experience in Futhark, but at a theoretical level, its\nadvantage compared to affine or uniqueness-based type systems is mainly in\nconvenience.
\nI intend to take a break from working on this part of the type system. It has\nsome restrictions for the sake of simplicity, and even some restrictions\ncompared to the formalisation. Maybe we will address these in the future. The\nmain limitation is that if you apply the identity function to a tuple, as in id (x,y), then you lose precision in the aliasing information, as the resulting\ntuple will be treated as having mutually aliased components. The formalisation\ndoes track this precisely, but I left it out of the compiler implementation for\nsimplicity. We’ll see whether anyone notices.