The Wyn Language Specification

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 accepted or produced by the function. For example:

def double<[n]>(a: [n]i32) [n]i32 = map(|x| x * 2, a)

A size parameter, [n], explicitly quantifies a size. The [n] parameter is not passed explicitly when calling the function; instead its value is implicitly deduced from the arguments. An array type can contain an anonymous size, e.g. []i32, for which the type checker invents a fresh size parameter — every array has a size in the type system. In return-type position this can produce an existential size that is not known until the function is fully applied. For example, filter has a return type along these lines:

filter : <[n], A>(A -> bool, [n]A) -> ?k. [k]A

Sizes may be any expression of type i64 that does not consume any free variables. Size parameters can be used as ordinary i64 variables within their scope. The type checker verifies that the program obeys any constraints imposed by size annotations.

Size-dependent types are supported, as the names of value 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) produces a value of type [10]i32.

Whenever a type [e]t is written, e must be a well-typed expression of type i64 in scope (possibly by referencing a name 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, filter has a type roughly like:

filter : <[n], A>(A -> bool, [n]A) -> ?k. [k]A

The function returns an array of some existential size k that cannot be known in advance.

When an application filter(p, xs) is encountered, the result is typed [k]A, 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.

In general, unknown sizes are produced whenever the true size cannot be expressed. The following lists all sources of unknown sizes.

Size going out of scope

An unknown size is created when 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.

Computed expression passed as a size argument

The type of replicate(e, 0) should be [e]i32, but if e is not valid as a size expression this cannot be expressed. 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) produces an unknown size.

Complex slicing

Most complex array slicing, such as xs[a..b], has an unknown size. Exceptions are listed in the reference for slice expressions.

Complex ranges

Most complex ranges, such as a..<b, 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, given filter’s type:

filter : <[n], A>(A -> bool, [n]A) -> ?k. [k]A

an application filter(f, xs) causes the type checker to invent a fresh unknown size k', and the actual type for that application is [k']A.

Branches of if return arrays of different sizes

When an if (or match) expression has branches that return arrays of different sizes, the differing sizes are replaced with fresh unknown sizes. For example:

if b then [[1, 2], [3, 4]]
     else [[5, 6]]

This expression has type [k][2]i32 for some fresh k.

Important: the check for differing sizes is performed when first encountering the if or match during type checking. At that point the type checker may not yet realise that the two sizes are equal, even though constraints later in the function force them to be. Adding type annotations resolves this.

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. Similarly to conditionals, the type checker may sometimes be too conservative in concluding that a size might change during the loop; adding type annotations to the loop parameter can resolve this.

Size Coercion

Size coercion, written with :>, performs a runtime-checked coercion of one size to another. It is the escape hatch from the size type system — useful when a value has an unknown size that the programmer knows is equal to some named size:

def take_n<A>(n: i64, xs: []A) [n]A =
  xs[..n] :> [n]A

Here xs[..n] has an unknown size (slicing produces an existential size; see Unknown Sizes), and :> [n]A asserts that the slice’s size is in fact n. The assertion is checked at run-time.

Causality Restriction

Conceptually, size parameters are assigned their values by reading the sizes of concrete values passed as parameters. Every size parameter must therefore appear as the size of some parameter. The following is an error:

def f<[n]>(x: i32) i32 = i32.i64(n)   -- `n` is never bound by a param

The following is not an error:

def f<[n]>(g: [n]i32 -> [n]i32) i32 = ???

…but using this function comes with a constraint: whenever an application f(x) occurs, the value of the size parameter must be inferable. The value must have been used as the size of an array before the f(x) application is encountered. The notion of “before” is subtle since there is no overall evaluation order on a Wyn expression — only that a let-binding is evaluated before its body, the argument to a function is evaluated before the function itself, and the left operand of an operator is evaluated before the right.

The causality restriction only matters when a function has a size parameter whose first use is not as a concrete array size. It does not apply to uses of the following function, for example:

def f<[n]>(arr: [n]i32, g: [n]i32 -> [n]i32) [n]i32 = g(arr)

…because the value of n can be read directly from arr’s size.

Empty Array Literals

Just as with size-polymorphic functions, constructing an empty array requires knowing the exact size of the (missing) elements. In the following program the elements of a are constrained to have the same type as the elements of b, but b’s element sizes are not known at the time a is constructed:

def main(b: bool, xs: []i32) bool =
  let a: [][]i32 = [] in
  let b = [filter(|x| x > 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. The following is illegal:

type sum = #foo([]i32) | #bar([]i32)

def main(xs: *[]i32) i32 =
  let v: sum = #foo(xs) in
  xs[0]

Modules

When matching a module against a module type (see Modules), a non-lifted abstract type (one declared with type rather than type^) may not be implemented by a type abbreviation that contains any existential sizes. This ensures that, given:

module m : { type t } = …

an array of values of type m.t can always be constructed without risking irregularity.

Higher-order Functions

When a higher-order function expects a function argument whose output is itself an array, the per-call output size must be the same for every invocation. This is why map produces a regular array: its function argument has type A -> B, where B must be a fixed-size type, so every element of the input maps to a result of the same shape and the output stays rectangular.

Operators whose result size genuinely varies per call — filter, for example, where each invocation may keep a different number of elements — produce existentially-sized results that do not feed back into a map-like operator without first being materialised.

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 is replaced with an existential size. Usually this is harmless, but it means an expression like the following is ill-typed:

map(|xs: [m]i32| iota(length(xs)), xss)

Here length(xs) gives rise to some fresh size k. The lambda is then assigned the type [m]i32 -> [k]i32, which is immediately rewritten to [m]i32 -> ?k. [k]i32 because k was generated inside the lambda body. A function of this type cannot be passed to map, as explained above. The fix is to bind the length to a name in the enclosing scope before the lambda is constructed.