Size Types
Wyn supports a system of size-dependent types that statically checks that the sizes of arrays passed to a function are compatible.
Whenever a pattern occurs (in let, loop, and function parameters), as well as in return types, the types of the bindings express invariants about the shapes of arrays that are accepted or produced by the function. For example:
def f [n] (a: [n]i32) (b: [n]i32): [n]i32 =
map2 (+) a b
We use a size parameter, [n], to explicitly quantify a size. The [n] parameter is not explicitly passed when calling f. Rather, its value is implicitly deduced from the arguments passed for the value parameters. An array type can contain anonymous sizes, e.g. []i32, for which the type checker will invent fresh size parameters, which ensures that all arrays have a size. On the right-hand side of a function arrow (“return types”), this results in an existential size that is not known until the function is fully applied, e.g:
sig filter [n] 'a : (p: a -> bool) -> (as: [n]a) -> ?[k].[k]a
Sizes can be any expression of type i64 that does not consume any free variables. Size parameters can be used as ordinary variables of type i64 within the scope of the parameters. The type checker verifies that the program obeys any constraints imposed by size annotations.
Size-dependent types are supported, as the names of parameters can be used in the return type of a function:
def replicate 't (n: i64) (x: t): [n]t = ...
An application replicate 10 0 will have type [10]i32.
Whenever we write a type [e]t, e must be a well-typed expression of type i64 in scope (possibly by referencing names bound as a size parameter).
Unknown Sizes
There are cases where the type checker cannot assign a precise size to the result of some operation. For example, the type of filter is:
sig filter [n] 'a : (a -> bool) -> [n]t -> ?[m].[m]t
The function returns of an array of some existential size m, but it cannot be known in advance.
When an application filter p xs is found, the result will be of type [k]t, where k is a fresh unknown size that is considered distinct from every other size in the program. It is sometimes necessary to perform a size coercion (see Size coercion) to convert an unknown size to a known size.
Generally, unknown sizes are constructed whenever the true size cannot be expressed. The following lists all possible sources of unknown sizes.
Size going out of scope
An unknown size is created in some cases when the a type references a name that has gone out of scope:
match ...
case #some c -> replicate c 0
The type of replicate c 0 is [c]i32, but since c is locally bound, the type of the entire expression is [k]i32 for some fresh k.
Consuming expression passed as function argument
The type of replicate e 0 should be [e]i32, but if e is an expression that is not valid as a size, this is not expressible. Therefore an unknown size k is created and the size of the expression becomes [k]i32.
Compound expression used as range bound
While a simple range expression such as 0..<n can be assigned type [n]i32, a range expression 0..<(n+1) will give produce an unknown size.
Complex slicing
Most complex array slicing, such as xs[a:b], will have an unknown size. Exceptions are listed in the reference for slice expressions.
Complex ranges
Most complex ranges, such as a..<b, will have an unknown size. Exceptions exist for general ranges and “upto” ranges.
Existential size in function return type
Whenever the result of a function application has an existential size, that size is replaced with a fresh unknown size variable.
For example, filter has the following type:
sig filter [n] 'a : (p: a -> bool) -> (as: [n]a) -> ?[k].[k]a
For an application filter f xs, the type checker invents a fresh unknown size k', and the actual type for this specific application will be [k']a.
Branches of if return arrays of different sizes
When an if (or match) expression has branches that returns array of different sizes, the differing sizes will be replaced with fresh unknown sizes. For example:
if b then [[1,2], [3,4]]
else [[5,6]]
This expression will have type [k][2]i32, for some fresh k.
Important: The check whether the sizes differ is done when first encountering the if or match during type checking. At this point, the type checker may not realise that the two sizes are actually equal, even though constraints later in the function force them to be. This can always be resolved by adding type annotations.
An array produced by a loop does not have a known size
If the size of some loop parameter is not maintained across a loop iteration, the final result of the loop will contain unknown sizes. For example:
loop xs = [1] for i < n do xs ++ xs
Similar to conditionals, the type checker may sometimes be too cautious in assuming that some size may change during the loop. Adding type annotations to the loop parameter can be used to resolve this.
Size Coercion
Size coercion, written with :>, can be used to perform a runtime-checked coercion of one size to another. This can be useful as an escape hatch in the size type system:
def concat_to 'a (m: i32) (a: []a) (b: []a) : [m]a =
a ++ b :> [m]a
Causality Restriction
Conceptually, size parameters are assigned their value by reading the sizes of concrete values passed along as parameters. This means that any size parameter must be used as the size of some parameter. This is an error:
def f [n] (x: i32) = n
The following is not an error:
def f [n] (g: [n]i32 -> [n]i32) = ...
However, using this function comes with a constraint: whenever an application f x occurs, the value of the size parameter must be inferable. Specifically, this value must have been used as the size of an array before the f x application is encountered. The notion of “before” is subtle, as there is no evaluation ordering of a Wyn expression, except that a let-binding is always evaluated before its body, the argument to a function is always evaluated before the function itself, and the left operand to an operator is evaluated before the right.
The causality restriction only occurs when a function has size parameters whose first use is not as a concrete array size. For example, it does not apply to uses of the following function:
def f [n] (arr: [n]i32) (g: [n]i32 -> [n]i32) = ...
This is because the proper value of n can be read directly from the actual size of the array.
Empty Array Literals
Just as with size-polymorphic functions, when constructing an empty array, we must know the exact size of the (missing) elements. For example, in the following program we are forcing the elements of a to be the same as the elements of b, but the size of the elements of b are not known at the time a is constructed:
def main (b: bool) (xs: []i32) =
let a = [] : [][]i32
let b = [filter (>0) xs]
in a[0] == b[0]
The result is a type error.
Sum Types
When constructing a value of a sum type, the compiler must still be able to determine the size of the constructors that are not used. This is illegal:
type sum = #foo ([]i32) | #bar ([]i32)
def main (xs: *[]i32) =
let v : sum = #foo xs
in xs
Modules
When matching a module with a module type (see Modules), a non-lifted abstract type (i.e. one that is declared with type rather than type^) may not be implemented by a type abbreviation that contains any existential sizes. This is to ensure that if we have the following:
module m : { type t } = ...
Then we can construct an array of values of type m.t without worrying about constructing an irregular array.
Higher-order Functions
When a higher-order function takes a functional argument whose return type is a non-lifted type parameter, any instantiation of that type parameter must have a non-existential size. If the return type is a lifted type parameter, then the instantiation may contain existential sizes. This is why the type of map guarantees regular arrays:
sig map [n] 'a 'b : (a -> b) -> [n]a -> [n]b
The type parameter b can only be replaced with a type that has non-existential sizes, which means they must be the same for every application of the function. In contrast, this is the type of the pipeline operator:
sig (|>) '^a -> '^b : a -> (a -> b) -> b
The provided function can return something with an existential size (such as filter).
A function whose return type has an unknown size
If a function (named or anonymous) is inferred to have a return type that contains an unknown size variable created within the function body, that size variable will be replaced with an existential size. In most cases this is not important, but it means that an expression like the following is ill-typed:
map(|xs| iota(length(xs)), xss : [n][m]i32)
This is because the (length xs) expression gives rise to some fresh size k. The lambda is then assigned the type [n]t -> [k]i32, which is immediately turned into [n]t -> ?[k].[k]i32 because k was generated inside its body. A function of this type cannot be passed to map, as explained before. The solution is to bind length to a name before the lambda.