Futhark 0.25.1 released
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 knowncorrect 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 uninterpreted 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_commin 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 sizedependent 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) =
0:i], xs[i:])
(xs[
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 =
3d (n*m) l k xs) unflatten n m (unflatten_