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 any module-local type indices occurring inside them would not geenrally be 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, which is applied at validation time.