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{array}{r}\begin{array}{lrrl}& \mathit{numtype}& ::=& \mathsf{i}\mathsf{32}|\mathsf{i}\mathsf{64}|\mathsf{f}\mathsf{32}|\mathsf{f}\mathsf{64}\end{array}\end{array}$$

The types $\mathsf{i}\mathsf{32}$ and $\mathsf{i}\mathsf{64}$ classify 32 and 64 bit integers, respectively. Integers are not inherently signed or unsigned, their interpretation is determined by individual operations.

The types $\mathsf{f}\mathsf{32}$ and $\mathsf{f}\mathsf{64}$ 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, $|\mathsf{i}\mathsf{32}|=|\mathsf{f}\mathsf{32}|=32$ and $|\mathsf{i}\mathsf{64}|=|\mathsf{f}\mathsf{64}|=64$.

Vector Types

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

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{vectype}& ::=& \mathsf{v}\mathsf{128}\end{array}\end{array}$$

The type $\mathsf{v}\mathsf{128}$ 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, $|\mathsf{v}\mathsf{128}|=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 $\mathsf{extern}\mathsf{.}\mathsf{convert}\mathsf{\_}\mathsf{any}$ and $\mathsf{any}\mathsf{.}\mathsf{convert}\mathsf{\_}\mathsf{extern}$ instructions. That is, both type hierarchies are inhabited by an isomorphic set of values, but may have different, incompatible representations in practice.

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{absheaptype}& ::=& \mathsf{any}|\mathsf{eq}|\mathsf{i}\mathsf{31}|\mathsf{struct}|\mathsf{array}|\mathsf{none}\\ & & |& \mathsf{func}|\mathsf{nofunc}\\ & & |& \mathsf{exn}|\mathsf{noexn}\\ & & |& \mathsf{extern}|\mathsf{noextern}\\ & & |& \dots \\ & \mathit{heaptype}& ::=& \mathit{absheaptype}|\mathit{typeuse}\\ & \mathit{typeuse}& ::=& \mathit{typeidx}|\dots \end{array}\end{array}$$

A heap type is either abstract or concrete. A concrete heap type consists of a type use, which is a type index. It classifies an object of the respective type defined in a module. Abstract types are denoted by individual keywords.

The type $\mathsf{func}$ denotes the common supertype of all function types, regardless of their concrete definition. Dually, the type $\mathsf{nofunc}$ denotes the common subtype of all function types, regardless of their concrete definition. This type has no values.

The type $\mathsf{exn}$ denotes the common supertype of all exception references. This type has no concrete subtypes. Dually, the type $\mathsf{noexn}$ denotes the common subtype of all forms of exception references. This type has no values.

The type $\mathsf{extern}$ denotes the common supertype of all external references received through the embedder. This type has no concrete subtypes. Dually, the type $\mathsf{noextern}$ denotes the common subtype of all forms of external references. This type has no values.

The type $\mathsf{any}$ denotes the common supertype of all aggregate types, as well as possibly abstract values produced by internalizing an external reference of type $\mathsf{extern}$. Dually, the type $\mathsf{none}$ denotes the common subtype of all forms of aggregate types. This type has no values.

The type $\mathsf{eq}$ is a subtype of $\mathsf{any}$ that includes all types for which references can be compared, i.e., aggregate values and $\mathsf{i}\mathsf{31}$.

The types $\mathsf{struct}$ and $\mathsf{array}$ denote the common supertypes of all structure and array aggregates, respectively.

The type $\mathsf{i}\mathsf{31}$ denotes unboxed scalars, that is, integers injected into references. Their observable value range is limited to 31 bits.

Note

Values of type $\mathsf{i}\mathsf{31}$ are 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 one bit is reserved. Since this type is to be reliably unboxed on all hardware platforms supported by WebAssembly, it cannot be wider than 32 bits minus the tag bit.

Although the types $\mathsf{none}$, $\mathsf{nofunc}$, $\mathsf{noexn}$, and $\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, $(\mathsf{ref}\mathsf{null}\mathsf{nofunc})$ is the generic type of a null reference compatible with all function reference types.

The syntax of abstract heap types and type uses 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{array}{r}\begin{array}{lrrl}& \mathit{reftype}& ::=& \mathsf{ref}{\mathsf{null}}^{?}\mathit{heaptype}\end{array}\end{array}$$

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

In addition, a reference type of the form $\mathsf{ref}\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 but not in memories.

Conventions

• The reference type $\mathsf{anyref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{any})$.

• The reference type $\mathsf{eqref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{eq})$.

• The reference type $\mathsf{i}\mathsf{31}\mathsf{ref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{i}\mathsf{31})$.

• The reference type $\mathsf{structref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{struct})$.

• The reference type $\mathsf{arrayref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{array})$.

• The reference type $\mathsf{funcref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{func})$.

• The reference type $\mathsf{exnref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{exn})$.

• The reference type $\mathsf{externref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{extern})$.

• The reference type $\mathsf{nullref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{none})$.

• The reference type $\mathsf{nullfuncref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{nofunc})$.

• The reference type $\mathsf{nullexnref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\mathsf{noexn})$.

• The reference type $\mathsf{nullexternref}$ is an abbreviation for $(\mathsf{ref}\mathsf{null}\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{array}{r}\begin{array}{lrrl}& \mathit{consttype}& ::=& \mathit{numtype}|\mathit{vectype}\\ & \mathit{valtype}& ::=& \mathit{numtype}|\mathit{vectype}|\mathit{reftype}|\dots \end{array}\end{array}$$

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{array}{r}\begin{array}{lrrl}& \mathit{resulttype}& ::=& \mathit{list}(\mathit{valtype})\end{array}\end{array}$$

Function Types

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

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{functype}& ::=& \mathit{resulttype}\to \mathit{resulttype}\end{array}\end{array}$$

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, possibly packed fields. Structures are heterogeneous, but require static indexing, while arrays need to be homogeneous, but allow dynamic indexing.

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{structtype}& ::=& \mathit{list}(\mathit{fieldtype})\\ & \mathit{arraytype}& ::=& \mathit{fieldtype}\\ & \mathit{fieldtype}& ::=& {\mathsf{mut}}^{?}\mathit{storagetype}\\ & \mathit{storagetype}& ::=& \mathit{valtype}|\mathit{packtype}\\ & \mathit{packtype}& ::=& \mathsf{i}\mathsf{8}|\mathsf{i}\mathsf{16}\end{array}\end{array}$$

Conventions

• The notation $|t|$ for bit width extends to packed types as well, that is, $|\mathsf{i}\mathsf{8}|=8$ and $|\mathsf{i}\mathsf{16}|=16$.

• The auxiliary function $\mathrm{unpack}$ maps a storage type to the value type obtained when accessing a field:

  $$\begin{array}{r}\begin{array}{lll}\mathrm{unpack}(\mathit{valtype})& =& \mathit{valtype}\\ \mathrm{unpack}(\mathit{packtype})& =& \mathsf{i}\mathsf{32}\end{array}\end{array}$$

Composite Types

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

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{comptype}& ::=& \mathsf{struct}\mathit{structtype}\\ & & |& \mathsf{array}\mathit{arraytype}\\ & & |& \mathsf{func}\mathit{functype}\end{array}\end{array}$$

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{array}{r}\begin{array}{lrrl}& \mathit{rectype}& ::=& \mathsf{rec}\mathit{list}(\mathit{subtype})\\ & \mathit{subtype}& ::=& \mathsf{sub}{\mathsf{final}}^{?}{\mathit{typeuse}}^{\ast }\mathit{comptype}\\ & \mathit{typeuse}& ::=& \mathit{typeidx}|\dots \end{array}\end{array}$$

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

The syntax of type uses representing these type indices is later extended with additional forms for the purpose of specifying validation and execution.

Address Type

Address types are a subset of number types that classify the values that can be used as offsets into memories and tables.

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{addrtype}& ::=& \mathsf{i}\mathsf{32}|\mathsf{i}\mathsf{64}\end{array}\end{array}$$

Conventions

The minimum of two address types is defined as the address type whose bit width is the minimum of the two.

$$\begin{array}{r}\begin{array}{lcll}\min ({\mathit{at}}_1,{\mathit{at}}_2)& =& {\mathit{at}}_1& \text{if}|{\mathit{at}}_1|\le |{\mathit{at}}_2|\\ \min ({\mathit{at}}_1,{\mathit{at}}_2)& =& {\mathit{at}}_2& \text{otherwise}\end{array}\end{array}$$

Limits

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

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{limits}& ::=& [\mathit{u}\mathit{64}..\mathit{u}\mathit{64}]\end{array}\end{array}$$

Memory Types

Memory types classify linear memories and their size range.

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{memtype}& ::=& \mathit{addrtype}\mathit{limits}\mathsf{page}\end{array}\end{array}$$

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{array}{r}\begin{array}{lrrl}& \mathit{tabletype}& ::=& \mathit{addrtype}\mathit{limits}\mathit{reftype}\end{array}\end{array}$$

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{array}{r}\begin{array}{lrrl}& \mathit{globaltype}& ::=& {\mathsf{mut}}^{?}\mathit{valtype}\end{array}\end{array}$$

Element Types

Element types classify element segments by the reference type of its elements.

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{elemtype}& ::=& \mathit{reftype}\end{array}\end{array}$$

Data Types

Data types classify data segments. Since the contents of a data segment requires no further classification, they merely consist of a universal marker $\mathsf{ok}$ indicating well-formedness.

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{datatype}& ::=& \mathsf{ok}\end{array}\end{array}$$

External Types

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

$$\begin{array}{r}\begin{array}{lrrl}& \mathit{externtype}& ::=& \mathsf{func}\mathit{typeuse}|\mathsf{global}\mathit{globaltype}|\mathsf{table}\mathit{tabletype}|\mathsf{mem}\mathit{memtype}|\mathsf{tag}\mathit{typeuse}\end{array}\end{array}$$

For functions and tags, the type index has to refer to the definition of a function type. In the case of a tag, the parameters of the function type define the list of values associated with the exception thrown with this tag. The result type is empty for exception tags.

Note

Future versions of WebAssembly may have additional uses for tags, and may allow non-empty result types in the function types of tags.

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:

$$\begin{array}{r}\begin{array}{lcl}\mathrm{funcs}(ϵ)& =& ϵ\\ \mathrm{funcs}((\mathsf{func}\mathit{dt}){\mathit{xt}}^{\ast })& =& \mathit{dt}\mathrm{funcs}({\mathit{xt}}^{\ast })\\ \mathrm{funcs}(\mathit{externtype}{\mathit{xt}}^{\ast })& =& \mathrm{funcs}({\mathit{xt}}^{\ast })& \text{otherwise}\\ \mathrm{tables}(ϵ)& =& ϵ\\ \mathrm{tables}((\mathsf{table}\mathit{tt}){\mathit{xt}}^{\ast })& =& \mathit{tt}\mathrm{tables}({\mathit{xt}}^{\ast })\\ \mathrm{tables}(\mathit{externtype}{\mathit{xt}}^{\ast })& =& \mathrm{tables}({\mathit{xt}}^{\ast })& \text{otherwise}\\ \mathrm{mems}(ϵ)& =& ϵ\\ \mathrm{mems}((\mathsf{mem}\mathit{mt}){\mathit{xt}}^{\ast })& =& \mathit{mt}\mathrm{mems}({\mathit{xt}}^{\ast })\\ \mathrm{mems}(\mathit{externtype}{\mathit{xt}}^{\ast })& =& \mathrm{mems}({\mathit{xt}}^{\ast })& \text{otherwise}\\ \mathrm{globals}(ϵ)& =& ϵ\\ \mathrm{globals}((\mathsf{global}\mathit{gt}){\mathit{xt}}^{\ast })& =& \mathit{gt}\mathrm{globals}({\mathit{xt}}^{\ast })\\ \mathrm{globals}(\mathit{externtype}{\mathit{xt}}^{\ast })& =& \mathrm{globals}({\mathit{xt}}^{\ast })& \text{otherwise}\\ \mathrm{tags}(ϵ)& =& ϵ\\ \mathrm{tags}((\mathsf{tag}\mathit{jt}){\mathit{xt}}^{\ast })& =& \mathit{jt}\mathrm{tags}({\mathit{xt}}^{\ast })\\ \mathrm{tags}(\mathit{externtype}{\mathit{xt}}^{\ast })& =& \mathrm{tags}({\mathit{xt}}^{\ast })& \text{otherwise}\end{array}\end{array}$$