Futhark 0.25.1 released

Posted on July 6, 2023 by Troels Henriksen

Futhark 0.25.1 has escaped (full changelog here) and is coming to a package manager near you (at least if you are close to one of these). This is a major release - not just because of the version number, which tends to change mostly when we remove or change some obscure prelude function - but because the language has actually grown a cool new feature.

Specifically, this release adds arbitrary size expressions, which allows us to finally provide the right type for concatenation:

val (++) [n][m] 't : [n]t -> [m]t -> [n+m]t

Most of the details are in the post linked above, and even more here.

This release took longer than usual because we wanted to make sure that our approach is sound and useful. Along the way we even undertook to separate alias checking from tyep checking in order to simplify the latter, so its correctness (or lack of same) would be clearer.

As part of our work, we have adapted our entire test and benchmark suite, as well as various Futhark libraries, to the new rules. This was surprisingly painless - in retrospect not a great surprise, as we are extending the flexibility of the type system - but we’ve been accustomed to breaking changes being painful. Indeed, almost all of the pain is due to removing certain prelude functions that were previously used to work around type system limitations (more on that below).

What next?

I’m looking forward to figuring out what kind of programming techniques are made possible as Futhark inches ever closer to dependent types. (Some might argue we should investigate this before extending the language.) While more precise types for ++ and flatten and such is useful, it’s not really cool. The most cool application I have seen (which is perhaps not terribly useful) is that we can define a Futhark library for proving arithmetic identities, and then use that to perform known-correct coercions of array sizes. Suppose we have an abstract type

type eq[n][m]

where a value of type eq[a][b] encodes a proof that a and b are equal. We might then provide some standard axioms such as reflexivity:

val refl [n] : eq[n][n]

Or commutativity:

val comm [n][m] : eq[n][m] -> eq[m][n]

Or transitivity:

val trans [n][m][k] : eq[n][m] -> eq[m][k] -> eq[n][k]

And then things like the commutativity of addition:

val plus_comm [a][b] : eq[a+b][b+a]

As long as we make sure that the eq type is abstract, meaning the programmer cannot construct an eq[a][b] for any arbitrary a and b, but have to go through our functions, we can trust that it really encodes a valid equality. That can be used to ensure that a coercion function is only used when equality has been proven:

val coerce [n][m]'t : eq[n][m] -> [n]t -> [m]t

We can use the module system to ensure this abstraction. This is the full module:

module meta: {
  type eq[n][m]

  val coerce [n][m]'t : eq[n][m] -> [n]t -> [m]t

  val refl [n] : eq[n][n]
  val comm [n][m] : eq[n][m] -> eq[m][n]
  val trans [n][m][k] : eq[n][m] -> eq[m][k] -> eq[n][k]

  val plus_comm [a][b] : eq[a+b][b+a]
  val plus_assoc [a][b][c] : eq[(a+b)+c][a+(b+c)]
  val plus_lhs [a][b][c] : eq[a][b] -> eq[a+c][b+c]
  val plus_rhs [a][b][c] : eq[c][b] -> eq[a+c][a+b]
} = {
  type eq[n][m] = [0][n][m]()

  def coerce [n][m]'t (_: eq[n][m]) (a: [n]t) = a :> [m]t

  def refl = []
  def comm _ = []
  def trans _ _ = []

  def plus_comm = []
  def plus_assoc = []
  def plus_lhs _ = []
  def plus_rhs _ = []
}

Note how the eq[n][m] type definition does not actually contain anything interesting - merely an empty array. It acts only as a witness for the sizes n and m.

We can then use this meta module to show that a concatenation (xs++ys)++zs has the same size as a concatenation ys++(xs++zs) - this is not something the type checker can do on its own, as it treats functions in size expressions as un-interpreted constants. The entire thing looks like this:

def f [n][m][l] (xs: [n]i32) (ys: [m]i32) (zs: [l]i32) =
  let proof : meta.eq[m+(n+l)][(n+m)+l] =
    meta.comm meta.plus_assoc `meta.trans` meta.plus_lhs meta.plus_comm
  in zip ((xs ++ ys) ++ zs) (meta.coerce proof (ys ++ (xs ++ zs)))

While it’s cool that this works (at least I think so), I’m not entirely sure it’s all that useful. Humans are really not meant to prove basic arithmetic identities all the time - this kind of stuff screams out for automation. This is why we are now also investing a form of refinement typing where the size-dependent types are used for precisely carrying around the syntactic form of sizes, and checking of semantic equivalences is done by some kind of arithmetic solver. That’ll probably be the topic of a blog post or two in the future.

Compatibility shims

The code below contains definitions of prelude functions that changed their type, or were removed, since Futhark 0.24.3, with their old types. I’ve not included functions that were previously existential and were simply made more precise (++, concat, flatten), as these should still work with older code.

def split [n] 't (i: i64) (xs: [n]t): ([i]t, []t) =
  (xs[0:i], xs[i:])

def concat_to [n] [m] 't (k: i64) (xs: [n]t) (ys: [m]t): *[k]t =
  sized k (concat xs ys)

def flatten_to [n][m] 't (l: i64) (xs: [n][m]t): [l]t =
  sized l (flatten xs)

def unflatten [p] 't (n: i64) (m: i64) (xs: [p]t): [n][m]t =
  unflatten (sized (n*m) xs)

def unflatten_3d [p] 't (n: i64) (m: i64) (l: i64) (xs: [p]t): [n][m][l]t =
  unflatten n m (unflatten (n*m) l xs)

def unflatten_4d [p] 't (n: i64) (m: i64) (l: i64) (k: i64) (xs: [p]t): [n][m][l][k]t =
  unflatten n m (unflatten_3d (n*m) l k xs)