Types¶

Various entities in WebAssembly are classified by types. Types are checked during validation, instantiation, and possibly execution.

Number Types¶

Number types classify numeric values.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{number type} & \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}} &::=& \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}} ~|~ \href{../syntax/types.html#syntax-valtype}{\mathsf{i64}} ~|~ \href{../syntax/types.html#syntax-valtype}{\mathsf{f32}} ~|~ \href{../syntax/types.html#syntax-valtype}{\mathsf{f64}} \\ \end{array}\end{split}\]

The types \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) and \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i64}}\) classify 32 and 64 bit integers, respectively. Integers are not inherently signed or unsigned, their interpretation is determined by individual operations.

The types \(\href{../syntax/types.html#syntax-valtype}{\mathsf{f32}}\) and \(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}\) classify 32 and 64 bit floating-point data, respectively. They correspond to the respective binary floating-point representations, also known as single and double precision, as defined by the IEEE 754 standard (Section 3.3).

Number types are transparent, meaning that their bit patterns can be observed. Values of number type can be stored in memories.

Conventions¶

The notation \(|t|\) denotes the bit width of a number type \(t\). That is, \(|\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}| = |\href{../syntax/types.html#syntax-valtype}{\mathsf{f32}}| = 32\) and \(|\href{../syntax/types.html#syntax-valtype}{\mathsf{i64}}| = |\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}| = 64\).

Vector Types¶

Vector types classify vectors of numeric values processed by vector instructions (also known as SIMD instructions, single instruction multiple data).

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{vector type} & \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}} &::=& \href{../syntax/types.html#syntax-valtype}{\mathsf{v128}} \\ \end{array}\end{split}\]

The type \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) corresponds to a 128 bit vector of packed integer or floating-point data. The packed data can be interpreted as signed or unsigned integers, single or double precision floating-point values, or a single 128 bit type. The interpretation is determined by individual operations.

Vector types, like number types are transparent, meaning that their bit patterns can be observed. Values of vector type can be stored in memories.

Conventions¶

The notation \(|t|\) for bit width extends to vector types as well, that is, \(|\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}| = 128\).

Heap Types¶

Heap types classify objects in the runtime store. There are three disjoint hierarchies of heap types:

function types classify functions,
aggregate types classify dynamically allocated managed data, such as structures, arrays, or unboxed scalars,
external types classify external references possibly owned by the embedder.

The values from the latter two hierarchies are interconvertible by ways of the \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{extern.convert\_any}}\) and \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{any.convert\_extern}}\) instructions. That is, both type hierarchies are inhabited by an isomorphic set of values, but may have different, incompatible representations in practice.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{abstract heap type} & \href{../syntax/types.html#syntax-absheaptype}{\mathit{absheaptype}} &::=& \href{../syntax/types.html#syntax-heaptype}{\mathsf{func}} ~|~ \href{../syntax/types.html#syntax-heaptype}{\mathsf{nofunc}} \\&&|& \href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}} ~|~ \href{../syntax/types.html#syntax-heaptype}{\mathsf{noextern}} \\&&|& \href{../syntax/types.html#syntax-heaptype}{\mathsf{any}} ~|~ \href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}} ~|~ \href{../syntax/types.html#syntax-heaptype}{\mathsf{i31}} ~|~ \href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}} ~|~ \href{../syntax/types.html#syntax-heaptype}{\mathsf{array}} ~|~ \href{../syntax/types.html#syntax-heaptype}{\mathsf{none}} \\ \def\mathdef2883#1{{}}\mathdef2883{heap type} & \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} &::=& \href{../syntax/types.html#syntax-absheaptype}{\mathit{absheaptype}} ~|~ \href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}} \\ \end{array}\end{split}\]

A heap type is either abstract or concrete.

The abstract type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}\) denotes the common supertype of all function types, regardless of their concrete definition. Dually, the type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{nofunc}}\) denotes the common subtype of all function types, regardless of their concrete definition. This type has no values.

The abstract type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}}\) denotes the common supertype of all external references received through the embedder. This type has no concrete subtypes. Dually, the type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{noextern}}\) denotes the common subtype of all forms of external references. This type has no values.

The abstract type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}\) denotes the common supertype of all aggregate types, as well as possibly abstract values produced by internalizing an external reference of type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}}\). Dually, the type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{none}}\) denotes the common subtype of all forms of aggregate types. This type has no values.

The abstract type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}\) is a subtype of \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}\) that includes all types for which references can be compared, i.e., aggregate values and \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{i31}}\).

The abstract types \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}}\) and \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}}\) denote the common supertypes of all structure and array aggregates, respectively.

The abstract type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{i31}}\) denotes unboxed scalars, that is, integers injected into references. Their observable value range is limited to 31 bits.

Note

An \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{i31}}\) is not actually allocated in the store, but represented in a way that allows them to be mixed with actual references into the store without ambiguity. Engines need to perform some form of pointer tagging to achieve this, which is why 1 bit is reserved.

Although the types \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{none}}\), \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{nofunc}}\), and \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{noextern}}\) are not inhabited by any values, they can be used to form the types of all null references in their respective hierarchy. For example, \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{nofunc}})\) is the generic type of a null reference compatible with all function reference types.

A concrete heap type consists of a type index and classifies an object of the respective type defined in a module.

The syntax of heap types is extended with additional forms for the purpose of specifying validation and execution.

Reference Types¶

Reference types classify values that are first-class references to objects in the runtime store.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{reference type} & \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} &::=& \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} \\ \end{array}\end{split}\]

A reference type is characterised by the heap type it points to.

In addition, a reference type of the form \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht}\) is nullable, meaning that it can either be a proper reference to \(\mathit{ht}\) or null. Other references are non-null.

Reference types are opaque, meaning that neither their size nor their bit pattern can be observed. Values of reference type can be stored in tables.

Conventions¶

The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{anyref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{eqref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{i31ref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i31}}\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{structref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}}\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{arrayref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}}\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{funcref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{externref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}}\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{nullref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{none}}\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{nullfuncref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{nofunc}}\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{nullexternref}}\) is an abbreviation for \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{noextern}}\).

Value Types¶

Value types classify the individual values that WebAssembly code can compute with and the values that a variable accepts. They are either number types, vector types, or reference types.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{value type} & \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} &::=& \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}} ~|~ \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}} ~|~ \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \\ \end{array}\end{split}\]

The syntax of value types is extended with additional forms for the purpose of specifying validation.

Conventions¶

The meta variable \(t\) ranges over value types or subclasses thereof where clear from context.

Result Types¶

Result types classify the result of executing instructions or functions, which is a sequence of values, written with brackets.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{result type} & \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}} &::=& [\href{../syntax/conventions.html#syntax-vec}{\mathit{vec}}(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}})] \\ \end{array}\end{split}\]

Function Types¶

Function types classify the signature of functions, mapping a vector of parameters to a vector of results. They are also used to classify the inputs and outputs of instructions.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{function type} & \href{../syntax/types.html#syntax-functype}{\mathit{functype}} &::=& \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}} \href{../syntax/types.html#syntax-functype}{\rightarrow} \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}} \\ \end{array}\end{split}\]

Aggregate Types¶

Aggregate types describe compound objects consisting of multiple values. These are either structures or arrays, which both consist of a list of possibly mutable and possibly packed fields. Structures are heterogeneous, but require static indexing, while arrays need to be homogeneous, but allow dynamic indexing.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{structure type} & \href{../syntax/types.html#syntax-structtype}{\mathit{structtype}} &::=& \href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast \\ \def\mathdef2883#1{{}}\mathdef2883{array type} & \href{../syntax/types.html#syntax-arraytype}{\mathit{arraytype}} &::=& \href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}} \\ \def\mathdef2883#1{{}}\mathdef2883{field type} & \href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}} &::=& \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}} \\ \def\mathdef2883#1{{}}\mathdef2883{storage type} & \href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}} &::=& \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} ~|~ \href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}} \\ \def\mathdef2883#1{{}}\mathdef2883{packed type} & \href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}} &::=& \href{../syntax/types.html#syntax-storagetype}{\mathsf{i8}} ~|~ \href{../syntax/types.html#syntax-storagetype}{\mathsf{i16}} \\ \end{array}\end{split}\]

Conventions¶

The notation \(|t|\) for bit width extends to packed types as well, that is, \(|\href{../syntax/types.html#syntax-storagetype}{\mathsf{i8}}| = 8\) and \(|\href{../syntax/types.html#syntax-storagetype}{\mathsf{i16}}| = 16\).
The auxiliary function \(\href{../syntax/types.html#aux-unpacktype}{\mathrm{unpack}}\) maps a storage type to the value type obtained when accessing a field:

\[\begin{split}\begin{array}{lll} \href{../syntax/types.html#aux-unpacktype}{\mathrm{unpack}}(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}) &=& \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \\ \href{../syntax/types.html#aux-unpacktype}{\mathrm{unpack}}(\href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}) &=& \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}} \\ \end{array}\end{split}\]

Composite Types¶

Composite types are all types composed from simpler types, including function types and aggregate types.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{composite type} & \href{../syntax/types.html#syntax-comptype}{\mathit{comptype}} &::=& \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} ~|~ \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-structtype}{\mathit{structtype}} ~|~ \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-arraytype}{\mathit{arraytype}} \\ \end{array}\end{split}\]

Recursive Types¶

Recursive types denote a group of mutually recursive composite types, each of which can optionally declare a list of type indices of supertypes that it matches. Each type can also be declared final, preventing further subtyping.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{recursive type} & \href{../syntax/types.html#syntax-rectype}{\mathit{rectype}} &::=& \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast \\ \def\mathdef2883#1{{}}\mathdef2883{sub types} & \href{../syntax/types.html#syntax-subtype}{\mathit{subtype}} &::=& \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?~\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}^\ast~\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}} \\ \end{array}\end{split}\]

In a module, each member of a recursive type is assigned a separate type index.

The syntax of sub types is generalized for the purpose of specifying validation and execution.

Limits¶

Limits classify the size range of resizeable storage associated with memory types and table types.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{limits} & \href{../syntax/types.html#syntax-limits}{\mathit{limits}} &::=& \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}^? \} \\ \end{array}\end{split}\]

If no maximum is given, the respective storage can grow to any size.

Memory Types¶

Memory types classify linear memories and their size range.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{memory type} & \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} &::=& \href{../syntax/types.html#syntax-limits}{\mathit{limits}} \\ \end{array}\end{split}\]

The limits constrain the minimum and optionally the maximum size of a memory. The limits are given in units of page size.

Table Types¶

Table types classify tables over elements of reference type within a size range.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{table type} & \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} &::=& \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \\ \end{array}\end{split}\]

Like memories, tables are constrained by limits for their minimum and optionally maximum size. The limits are given in numbers of entries.

Global Types¶

Global types classify global variables, which hold a value and can either be mutable or immutable.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{global type} & \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} &::=& \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \\ \def\mathdef2883#1{{}}\mathdef2883{mutability} & \href{../syntax/types.html#syntax-mut}{\mathit{mut}} &::=& \href{../syntax/types.html#syntax-mut}{\mathsf{const}} ~|~ \href{../syntax/types.html#syntax-mut}{\mathsf{var}} \\ \end{array}\end{split}\]

External Types¶

External types classify imports and external values with their respective types.

\[\begin{split}\begin{array}{llrl} \def\mathdef2883#1{{}}\mathdef2883{external types} & \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} &::=& \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} ~|~ \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} ~|~ \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} ~|~ \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \\ \end{array}\end{split}\]

Conventions¶

The following auxiliary notation is defined for sequences of external types. It filters out entries of a specific kind in an order-preserving fashion:

\(\href{../syntax/types.html#syntax-externtype}{\mathrm{funcs}}(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast) = [\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}} ~|~ (\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}) \in \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast]\)
\(\href{../syntax/types.html#syntax-externtype}{\mathrm{tables}}(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast) = [\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} ~|~ (\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}) \in \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast]\)
\(\href{../syntax/types.html#syntax-externtype}{\mathrm{mems}}(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast) = [\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} ~|~ (\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}) \in \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast]\)
\(\href{../syntax/types.html#syntax-externtype}{\mathrm{globals}}(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast) = [\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} ~|~ (\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}) \in \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast]\)