The Wyn Language Specification

Compound Types and Values

Grammar

type ::= qualname
       | array_type
       | tuple_type
       | record_type
       | sum_type
       | function_type
       | type_application
       | existential_size

tuple_type ::= "(" ")" | "(" type ("," type)+ [","] ")"

array_type ::= "[" [exp] "]" type

sum_type ::= sum_variant ("|" sum_variant)*
sum_variant ::= constructor [ "(" type ("," type)* [","] ")" ]

record_type ::= "{" "}" | "{" fieldid ":" type ("," fieldid ":" type)* [","] "}"

type_application ::= type type_arg | "*" type
type_arg         ::= "[" [dim] "]" | type

function_type ::= param_type "->" type
param_type    ::= type | "(" name ":" type ")"

stringlit  ::= '"' stringchar* '"'
stringchar ::= <any source character except "\" or newline or double quotes>

existential_size ::= "?" ("[" name "]")+ "." type

Description

Compound types can be constructed based on the primitive types. The Wyn type system is entirely structural, and type abbreviations are merely shorthands. The only exception is abstract types whose definition has been hidden via the module system.

Tuple Types

A tuple value or type is written as a sequence of comma-separated values or types enclosed in parentheses. For example, (0, 1) is a tuple value of type (i32, i32). The elements of a tuple need not have the same type – the value (false, 1, 2.0) is of type (bool, i32, f32). A tuple element can also be another tuple, as in ((1,2),(3,4)), which is of type ((i32, i32), (i32, i32)). A tuple cannot have just one element, but empty tuples are permitted, although they are not very useful. Empty tuples are written () and are of type ().

Array Types

An array value is written as a sequence of zero or more comma-separated values enclosed in square brackets: [1, 2, 3]. An array type is written as [d]t, where t is the element type of the array, and d is an expression of type i64 indicating the number of elements in the array. We can elide d and write just [] (an anonymous size), in which case the size will be inferred.

As an example, an array of three integers could be written as [1, 2, 3], and has type [3]i32. An empty array is written as [], and its type is inferred from its use. When writing Wyn values for testing purposes, empty arrays are written empty([0]t) for an empty array of type [0]t.

Multi-dimensional arrays are supported in Wyn, but they must be regular, meaning that all inner arrays must have the same shape. For example, [[1,2], [3,4], [5,6]] is a valid array of type [3][2]i32, but [[1,2], [3,4,5], [6,7]] is not, because we cannot come up with integers m and n such that [m][n]i32 describes the array. The restriction to regular arrays is rooted in low-level concerns about efficient compilation.

Vector Types

A vector is a fixed-width aggregate of scalar components, written vecNT where N is the component count (2, 3, or 4) and T is the scalar element type — e.g. vec3f32, vec4i32. Vector literals use the @[...] syntax: let v: vec3f32 = @[1.0, 2.0, 3.0]. See Vector Types below for the full naming table, constructors, and swizzles.

Matrix Types

A matrix is a fixed-shape aggregate of scalar components, written matRxCT (rectangular) or matNT (square, equivalent to matNxNT). Supported dimensions are R, C ∈ {2, 3, 4}; element types are the primitive scalar types. Matrix literals use the @[[...], [...], ...] syntax. See Matrix Types below for naming and construction details.

Sum Types

Sum types are anonymous in Wyn, and are written as the constructors separated by vertical bars. Each constructor consists of a #-prefixed name and an optional parenthesised payload — a comma-separated list of payload types (or sub-patterns / sub-expressions, depending on the syntactic position). A constructor with no payload is written bare, with no parentheses.

Because sum types are structural, constructor names are not globally unique — they are tags inside a sum type, not declarations. The same name #left belongs to infinitely many possible sum types (#left(i32) | #right(f32), #left(bool) | #middle | #right, …), so a bare constructor expression like #left(3) is ambiguous in isolation. The type checker resolves it from context — the expected type at the use site, the type of an argument it’s being passed as, or an explicit annotation. When context doesn’t pin a single sum type down, an annotation is required:

let x: #left(i32) | #right(f32) = #left(3)

Note: Implementations are not required to optimize the representation of sum-typed values. A sum-typed value may carry storage for every constructor’s payload; sum types with multiple large-payload constructors can be costly.

Record Types

Records are mappings from field names to values, with the field names known statically. A tuple behaves in all respects like a record with numeric field names starting from zero, and vice versa. It is an error for a record type to name the same field twice. A trailing comma is permitted.

Records are structural: a field name x does not identify a single record type, so a bare projection r.x does not fully determine r’s type by itself. As with sum constructors, the type checker uses context — the inferred type of r from the surrounding expression, or an explicit annotation on r — to pick a single record type. When context doesn’t suffice, an annotation is required:

let r: { x: f32, y: f32 } = make_point() in r.x

Function Types

Functions are classified via function types, but they are not fully first class. See Higher-order functions for the details.

String Literals

Wyn has no first-class string type. A string literal ("...") is a lexical token accepted only in two non-expression positions: the path in import "..." and the linkage name in #[linked("...")]. Writing a string where a value is expected is a syntax error.

Existential Size Quantifiers

An existential size quantifier brings an unknown size into scope within a type. It is used to describe results whose size is not statically known — most commonly, the output of filter:

def is_even(x: i32) bool = x % 2 == 0

def evens(arr: [8]i32) ?k. [k]i32 =
    filter(is_even, arr)

The return type ?k. [k]i32 says “for some size k, an array of length k”. A caller of evens receives an array of unknown-but-fixed length; k is in scope within the type but cannot be statically determined by the caller.