Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Type Abbreviations

Grammar

type_bind  ::= ("type" | "type^" | "type~") name type_param* "=" type
type_param ::= "[" name "]" | "'" name | "'~" name | "'^" name

Description

Type abbreviations function as shorthands for the purpose of documentation or brevity. After a type binding type t1 = t2, the name t1 can be used as a shorthand for the type t2. Type abbreviations do not create distinct types: the types t1 and t2 are entirely interchangeable.

Lifted Types

If the right-hand side of a type contains existential sizes, it must be declared “size-lifted” with type~. If it (potentially) contains a function, it must be declared “fully lifted” with type^. A lifted type can also contain existential sizes.

Restrictions:

  • Lifted types cannot be put in arrays
  • Fully lifted types cannot be returned from conditional or loop expressions

Type Parameters

A type abbreviation can have zero or more parameters:

Size Parameters

A type parameter enclosed with square brackets is a size parameter, and can be used in the definition as an array size, or as a size argument to other type abbreviations. When passing an argument for a shape parameter, it must be enclosed in square brackets:

type two_intvecs [n] = ([n]i32, [n]i32)

def x: two_intvecs [2] = (iota 2, replicate 2 0)

When referencing a type abbreviation, size parameters work much like array sizes. Like sizes, they can be passed an anonymous size ([]). All size parameters must be used in the definition of the type abbreviation.

Type Parameters

A type parameter prefixed with a single quote is a type parameter. It is in scope as a type in the definition of the type abbreviation. Whenever the type abbreviation is used in a type expression, a type argument must be passed for the parameter. Type arguments need not be prefixed with single quotes:

type two_vecs [n] 't = ([n]t, [n]t)
type two_intvecs [n] = two_vecs [n] i32
def x: two_vecs [2] i32 = (iota 2, replicate 2 0)

Lifted Type Parameters

  • Size-lifted type parameter: prefixed with '~
  • Fully lifted type parameter: prefixed with '^

These have the same rules and restrictions as lifted type abbreviations.