Types

Execution has to check and compare types in a few places, such as executing \(\mathsf{call\_indirect}\) or instantiating modules.

It is an invariant of the semantics that all types occurring during execution are closed.

Note

Runtime type checks generally involve types from multiple modules or types not defined by a module at all, such that module-local type indices are not meaningful.

Instantiation

Any form of type can be instantiated into a closed type inside a module instance by substituting each type index \(x\) occurring in it with the corresponding defined type \({\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}{}[x]\).

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {{\href{../exec/types.html#type-inst}{\mathrm{clos}}}}_{{\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}}(t) & = & {t}{{}[ {\href{../valid/conventions.html#notation-subst}{\mathrel{:=}}}\, {{\mathit{dt}}^\ast} ]} & \quad \mbox{if}~ {{\mathit{dt}}^\ast} = {\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}} \\ \end{array}\end{split}\]

Note

This is the runtime equivalent to type closure.