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.
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.
Note: Explicit parametric type application at use sites is not yet supported by the reference implementation; an abbreviation with parameters can be declared but cannot currently be referenced with explicit arguments. The behaviour above is the intended spec.