Type Abbreviations
Grammar
type_bind ::= type_keyword name [generics] "=" type
type_keyword ::= "type" | "type~" | "type^"
generics ::= "<" generic_param ("," generic_param)* ">"
generic_param ::= "[" name "]" | UpperName
Description
A type abbreviation is a shorthand: after type t1 = t2, the name
t1 is interchangeable with the type t2. Type abbreviations do
not introduce distinct types; the abbreviation and its definition
denote the same type.
The bound name must start with a lowercase letter or underscore.
Uppercase identifiers in type position are reserved for type
parameters (see UpperName above).
Lifted Types
A type abbreviation must be marked size-lifted (type~) if its
right-hand side contains existential sizes, and fully lifted
(type^) if it (potentially) contains a function. A fully-lifted
type may also contain existential sizes.
type~ bag = ?n. [n]i32
def empty_bag: bag = []
type^ cmp = i32 -> i32 -> i32
def ascending: cmp = |x: i32, y: i32| x - y
def descending: cmp = |x: i32, y: i32| y - x
Restrictions:
- Lifted types cannot appear as array elements.
- Fully-lifted types cannot be returned from a conditional or loop expression.
Type Parameters
A type abbreviation may take size and/or type parameters via the
<...> generics list. Size parameters are written [n] and stand
in for array sizes; type parameters are uppercase identifiers and
stand in for arbitrary types:
type two_intvecs<[n]> = ([n]i32, [n]i32)
type two_vecs<[n], T> = ([n]T, [n]T)
When applying a parameterised abbreviation, size arguments go in
brackets (<[2]>) and type arguments are written bare (<i32>):
def x: two_intvecs<[2]> = ([1, 2], [3, 4])
def y: two_vecs<[2], i32> = ([1, 2], [3, 4])
All declared size parameters must appear in the definition.
Type constructors are first-order. An application must supply exactly one
argument for every declared parameter; type abbreviations cannot be partially
applied, passed as values, or abstracted over as higher-kinded parameters.
A size parameter accepts only a bracketed size argument such as [4], [n],
or []; an ordinary type parameter accepts a type. Arity and parameter-kind
mismatches are type errors.
Applications nest in the usual way. For example, outer<inner<i32>> is
accepted without whitespace between the two closing > characters.
Generic Type Applications
A generic type application names a type constructor followed by a fully saturated, comma-separated argument list in angle brackets. Ordinary type arguments are types; size arguments are enclosed in brackets.
pair<i32, bool>
two_vecs<[4], f32>
vector<[4], f32>
Type constructors are first-order. A type constructor cannot be used without its arguments, partially applied, passed as a value, or received through a type parameter. Each constructor fixes the number and kind of its arguments.