# Towards Size Types in Futhark

Futhark is not a large or particularly innovative language. We prefer to keep the novelties in the compiler, and only include language features that have already proven their worth in existing functional languages. One exception to this principle is *size annotations*, by which functions can express pre- and post-conditions on their arguments and return values. The classic example is matrix multiplication, where we can state that the innermost sizes of the array arguments must match, and that the shape of the result corresponds to the shape of the arguments:

```
let matmul [n][m][p] (x: [n][m]i32) (y: [m][p]i32): [n][p]i32 =
...
```

The leading `[n][m][p]`

are not ordinary parameters, but rather *size parameters*. They are not passed explicitly when calling `matmul`

, but rather inferred from the matrices passed for `x`

and `y`

. Size parameters are in scope inside the function definition as `i32`

-typed variables, which means we can define a function for returning the length of an array as thus:

`let length [n] 'a (xs: [n]a) = n`

The `length`

function (which is also polymorphic in the element type of `xs`

) does not use any of the values of `xs`

- it just returns the size `n`

.

We can even write functions where we state that the size of an array we return is the same as the value of one of our parameters, like in `iota`

:

`let iota (n: i32) : [n]i32 = 0..<n`

For simplicity, dimensions can be only names or constants, not compound expressions. I’ll return to the ramifications of this.

We have found size annotations to be very useful for understanding code, and it is one of the language features that Futhark programmers (few as they are) tend to single out as particularly useful, as size errors are some of the most common problems in array programming. Unfortunately, size annotations have one major flaw: they are not truly part of the type system. Currently, size annotations are ignored by the type checker and verified at run-time.

In this post, I will outline an idea for moving from size annotations to checkable *size types*. The design is not yet fully formed, as we shall see. While size types have a strong connection to dependent types, the way I intend to use them in Futhark are not quite the same as in truly dependently typed languages like Idris, so I cannot just take a design from the latest POPL paper. In particular, I want to preserve the Futhark current programming experience as much as possible, notably including preserving solid type inference. This is not so much because there is all that much Futhark code that I wish to avoid breaking, but because Futhark is currently a rather simple, accessible, and *fun* language, and I would like to keep it that way.

## Basic type inference

The idea behind size types is based on an extension of classic Hindley-Milner type inference. So first, let us review what that’s all about. There are two main concepts we must understand: *instantiation* and *let-generalisation*.

### Instantiation

We will get to type inference shortly. For now, consider an explicitly typed identity function in Futhark:

`let id 'a (x: a) : a = x`

This function is known to the type checker by the following *type scheme*:

`val id 'a : a -> a`

The type scheme contains all the information that is needed to check uses of the function. Specifically, the type scheme tells us that `id`

has a single *type parameter* (`a`

). Consider now an application:

`2 id `

where `i`

has type `i32`

. Note that an explicit argument is not provided for the type parameter. Whenever a reference to a polymorphic definition such as `id`

is encountered by the type checker, its type scheme is *instantiated*. The instantiation procedure generates a fresh *type variable* for each type parameter, and then replaces each type parameter in the type with its corresponding type variable. Type variables are a bit of machinery that stand in for currently unknown types. A type variable can be unified with another type, which will replace all instances of the type variable with the other type.

For example, in the application `id 2`

, the `id`

function might be instantiated by generating a fresh type variable `t0`

, and replacing `a`

with `t0`

in the type scheme of `id`

, such that the type of *this* instance of `id`

now has type `t0 -> t0`

. Note the absence of type parameters: these are only present in type *schemes*, not *types*. (Higher-ranked types are different, but these do not exist in Futhark.) Since we are applying `id`

to `2`

, the type checker will unify the parameter type of `id`

(`t0`

) with the type of `2`

(`i32`

), producing the substitution `t0 ⟼ i32`

, which is then applied whenever `t0`

occurs. Since `t0`

also occurs in the return type of `id`

, we find that the final type of `id 2`

is `i32`

.

### Let-generalisation

*Let-generalisation* can be seen as the dual to instantiation, in that it turns un-unified type variables into type parameters in order to infer polymorphic definitions. The idea is simple. Whenever we have a `let`

-binding

`let x = e...`

then if any type variables constructed while inferring the type of `e`

remain in the type of `e`

, those type variables are turned into type parameters when constructing the type scheme for `x`

.

For example, consider the following definition:

`let f x = x`

When new names are bound (here, the parameter `x`

), we generate a new type variable, say `tx`

. Hence, the body of `f`

has type `tx`

, and `f`

as a whole has type `tx -> tx`

, where `tx`

is a type variable. Let-generalisation finds all such type variables and turn them into type parameters for the type scheme of `f`

:

`val f 'tx : tx -> tx`

There need not be any relationship in naming between type parameters and type variables. In practice, type variables tend to have ugly internal names (because many of them are typically generated during type-checking nontrivial functions), while we would like inferred type parameters to have short and clean names. Thus, the compiler may perform some renaming before constructing the type scheme.

In practice, and in Futhark, let-generalisation is only done for `let`

-bindings of *functional* type. We shall later see an example where this causes some problems.

### Rigid type variables

The type variables discussed so far have been placeholders that could be replaced (through unification) with concrete types. We call such types *nonrigid*. In contrast, *rigid* types do not unify with anything but themselves. The most common source of rigid types are primitive types and explicit type parameters:

`let g 'a (x: a) : i32 = x`

Here we are writing a function that tries to turn an `a`

into an `i32`

. Clearly this should not be well typed. And indeed it is not: both `a`

and `i32`

are *rigid*, so they cannot be unified with each other.

As a contrast, consider this contrived function:

`let h 'a x : a = x`

Here the type checker will generate a nonrigid type variable `xa`

for `x`

, unify `xa`

with `a`

to produce the substitution `xa ⟼ a`

, and finally infer the following type scheme:

`let h 'a : a -> a`

Some presentations do not have the notion of rigid type variables at all - they simply consider them *types*, rather than type *variables*. However, for size types, it is convenient to treat them as a degenerate class of variables, as we shall see.

## Extending Hindley-Milner with Size Types

The basic idea is pretty simple: have *size variables* that act much as type variables, using the same unification machinery. We have a distinction between *rigid sizes*, which cannot unify with anything but themselves, and *nonrigid size variables*, which do unify. When unifying two array types `[d1]t1`

and `[d2]t2`

we unify `d1`

with `d2`

and `t1`

with `t2`

.

Consider the type of `zip`

:

`val zip [n] 'a 'b : [n]a -> [n]b -> [n](a,b)`

Now suppose that we are type-checking the following application:

` zip xs ys`

The type scheme of `zip`

is instantiated and each type- and size parameter replaced with a new non-rigid type variable. Let us say that post-instantiation, this occurrence of `zip`

has the following type:

` [d0]t1 -> [d0]t2 -> [d0](t1, t2)`

When checking the application of `zip`

to `xs`

, we have to unify the parameter type `[d0]t1`

with the type of `xs`

, which we will suppose is `[10]bool`

. The unification succeeds and produces the following substitutions:

```
10
d0 ⟼ t1 ⟼ bool
```

This means that we infer the type of `zip xs`

as `[10]t2 -> [10](bool, t2)`

. When we then try to apply this to `ys`

, unification will succeed only if the size of `ys`

can be unified with the constant size `10`

(so, `ys`

must be an 10 element array).

Let-generalisation functions more or less the same. Suppose we are type-checking the following `let`

-binding of a lambda abstraction:

`let f = \xs ys -> zip xs ys`

After unification, the right-hand side will be inferred to have type `[d0]t1 -> [d0]t2 -> [d0](t1, t2)`

, where `d0`

is a nonrigid size variable and `t1`

, and `t2`

are nonrigid type variables. Let-generalisation then takes place, turning the former into a size parameter, and the latter two into type parameters, yielding the following type scheme:

`val f [d0] 't1 't2 = [d0]t1 -> [d0]t2 -> [d0](t1, t2)`

When replacing a type variable with an array type, the dimensions of that array type are propagated as well. This has the consequence that if the following fully polymorphic function is called with two arrays, those arrays must have the same size:

`let pair 'a (x: a) (y: a) = (x, y)`

This restriction is actually already in place in Futhark (although by a different mechanism), and was added to slowly prepare the way for size types.

This simple mechanism is enough to handle a surprising majority of the cases that occur even in nontrivial Futhark programs. However, we also need to think about how to handle less well behaved programs.

### Unknowable sizes

Consider the `filter`

function, which removes those elements of an array for which some function returns false:

`val filter [n] 'a = (a -> bool) -> [n]a -> [?]a`

What should we put in place of the question mark? The only non-constant size available to use is `n`

, and that is clearly not correct. We call the size of such an array *existential*, based on the “∃” quantifier from logic: we know that the array must have *some* size, but we cannot know what it is until the function returns. To handle such cases, we just leave the dimension empty:

`val filter [n] 'a = (a -> bool) -> [n]a -> []a`

This is permitted *only* in declarations like type schemes and when annotating parameter types: when type-checking an expression, we would like to have the invariant that all array dimensions have a size, although that size may well be a size variable. To accomplish this, whenever we type-check an application of a function with empty dimensions in its return type, we instantiate those empty dimensions with new *rigid* size variables. The rigidity is crucial, as it means the shape of the array cannot match the shape of *any other array*. For example, in the expression

` zip (filter p xs) ys`

there is *no expression ``ys``* that would make this well-typed. In most cases, when we want to do something interesting with an array of existential size, we will have to insert an explicit *size coercion*. These coercions are dynamically checked, and change the type of the array as far as the type checker is concerned:

`10]bool) ys zip (filter p xs : [`

This convinces the type checker that `filter p xs`

has type `[10]bool`

. Only the sizes of each dimension may be changed this way - the rank and element type of the array must be as otherwise inferred. Size coercions are intended to be the *sole* syntactic construct that can fail at run-time with a shape error.

Similarly, we may have `if`

expressions where the two branches return arrays of two different sizes:

```
if b then iota 10
else iota 20
```

Those dimensions that do not match will have their size replaced with a rigid size variable.

Another case of rigid sizes occurs when a function with a size-dependent type is given an argument for its size parameter that cannot syntactically be a size. Consider again `iota`

:

`val iota : (n: i32) -> [n]i32`

The type of `iota x`

should be `[x]i32`

, but what about `iota (x+1)`

? Syntactically, there is no such thing as a type `[x+1]i32`

. While it is likely we may lift this restriction some day (it is in place to avoid having to solve complicated arithmetic problems during unification), for now such an application will result in a rigid size. A simple workaround is to `let`

-bind `x+1`

to a name and then passing that name to `iota`

.

### Unsolved Problems

All of this is work-in-progress. While I have a branch implementing most of this (and it is able to compile most of our benchmarks and tests), there are still unsolved problems in both implementation and concept. As an example of the latter, consider the following program:

`let f xs = zip (filter p xs) xs`

By the rules discussed so far, `xs`

will initially be given the type `[d0]t1`

, where `d0`

is a nonrigid size variable, `filter p xs`

will have type `[d1]t1`

where `d1`

is a *rigid* type variable, and then due to the `zip`

we will produce the substitution `d0 ⟼ d1`

, and so the whole type of `f`

will be `[d1]t1 -> [d1](t1, t2)`

, where `d1`

is a rigid size variable computed inside `f`

itself. Clearly this makes no sense. I think the rule is that it should be a type error for a rigid size variable to propagate into the type of something that is being `let`

-bound.

Another problem brought about by rigid size variables is the potential for time travel. Specifically, since Futhark allows term-level values to be extracted from types (remember `length`

from above), I am concerned that a type-based unification performed inside a control-flow path (`if`

branch) that is not executed at run-time, can influence the size of some array generated *outside* the `if`

. Suppose first that the function `concat`

has the following type:

`val concat [n] [m] 'a = [n]a -> [m]a -> []a`

Note that if we call `concat`

with two-dimensional arrays, the row sizes must match exactly, because they are identified by the same type parameter (`a`

).

Now ponder the following program:

```
let shape [n] [m] (xss: [n][m]i32) = (n, m)
let f (b: bool) (xs: []i32) =
let arr = [] -- Inferred as type [][]i32.
in if b
then shape (concat [filter p xs] arr)
else shape arr
```

What should `f false [1,2,3]`

return? Due to the `concat`

, we are forcing the row size of `arr`

to be the size of `filter p xs`

, which is a rigid size variable. However, if `b`

is false, then `filter p xs`

will never be run, yet we still inspect the size of `arr`

! I’m not quite sure how to handle this. Either we need to make `arr`

properly polymorphic (currently only functional bindings are let-generalised), or we need to institute rules for certain syntactic constructs (mostly array literals and related cases) that prevent unification with rigid size variables. The fundamental problem is that at run-time, we may need to construct an actual multidimensional array *right now*, and when that happens, we better have *actual* sizes for the dimensions available, and not just a promise that they’ll match the size of some other array that may or may not be computed in the future.

As a final problem, consider the type of `map`

:

`val map [n] 'a 'b : (a -> b) -> [n]a -> [n]b`

Should `map iota is`

be well typed? Probably not, since this would only work if all values of `is`

are the same. But how should this be prevented? Maybe type checking of function application should take a closer look at whether any dependent typing is going on in case of higher-order functions, but a clear rule has not yet crystallised.

### Perspective

I don’t think ironing out the kinks in size types is an insurmountable problem. Fundamentally, I think they are quite simple, and I’m perfectly willing to give up some completeness (and resorting to size coercions) in order to maintain simplicity and type inference. However, to fully convince myself and others, we may have to break open the big box of Greek letters, and actually prove some properties about the type system. I’ll get around to that once I figure out exactly what the rules are even supposed to *be*.

Promisingly, it took fairly little work to make sure most of our benchmarks type-check under the current prototype of size types. I had to fix only a few things, and in most cases I would say they even improved the style of the program. In a few cases, I even fixed real (but dormant) bugs. I think this is because size types more or less just codify what is already good Futhark coding practice.

There is of course also the risk that the type checker is simply buggy and is letting incorrect programs slip by. That’s the frustrating part about working on a type checker: your programs may type check, but that does not mean that the type checker is correct…