$$$$$$$$$$$$$$

$$$$$$

$$

$$$$

$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$

Metamodel

Goal

Define an architecture to represent a breadth of real-world entities as structured data (models). Specify two operations to act on models: reading and writing. Design a rich system of types, constraints, and invariants, such that any operation always yields a semantically correct model.

We will define the following concepts:

• values
• models
• identifiers
• references

Labels

Going forward, we will need to assign labels to values. To be able to refer to labels in mathematical notation, we define the set $\mathcal{L}$ of all labels. By convention, we will understand strings in formulas typeset in monospace font to be elements of $\mathcal{L}$, like $\mathtt{name}$ or $\mathtt{id}$.

Values

We denote the set of all model values $\mathbb{V}$. There are different kinds of values:

Numbers

A number is any of the rational numbers, which we denote $\mathbb{Q}$.

Examples:

• $-3$
• $0$
• $42$
• $\frac{11}{3}$
• $9223372036854775808$

Bags

A bag is a finite multiset of values. We denote the set of bags over a set $X$ as $\mathcal{B}\left(X\right)$.

Examples:

• $\{1,2,1,2\}$
• $\left\{42\right\}$
• $\left\{\right\}$
• $\{\{0,\left\{0\right\},0,1\},\{1,1\},0\}$

Lists

A list is a finite sequence of values. We denote the set of lists over a set $X$ as $X^{\ast }$.

Examples:

• $(1,2,3,4)$
• $(5,0,5)$
• $\left(\right)$
• $(\left(1\right),0,\left\{1\right\})$

Records

Records assign labels to values. They are finite, partial functions from labels to values. We denote the set of records over a set $X$ as $\left[\mathcal{L}{\stackrel{}{\rightharpoonup }}_{\mathrm{fin}}X\right]$.

Examples:

• $[\mathtt{count}\mapsto 42]$
• $[\mathtt{dice}\mathtt{\_}\mathtt{rolls}\mapsto \{3,3,1,6\},\mathtt{ball}\mathtt{\_}\mathtt{picks}\mapsto (0,0,1,1,0)]$

Layered Construction

The value kinds above are mutually recursive: bags, lists, and records contain values, which themselves may be bags, lists, or records. To give this a well-defined foundation, we construct $\mathbb{V}$ in layers.

Definition (Value Hierarchy). We define an ascending sequence of sets $({\mathbb{V}}_n{)}_{n\in \mathbb{N}}$ by induction:

$$\begin{array}{rl}{\mathbb{V}}_0& :=\mathbb{Q}\\ {\mathbb{V}}_{n+1}& :={\mathbb{V}}_n\bigsqcup \mathcal{B}\left({\mathbb{V}}_n\right)\bigsqcup {\mathbb{V}}_n^{\ast }\bigsqcup \left[\mathcal{L}{\stackrel{}{\rightharpoonup }}_{\mathrm{fin}}{\mathbb{V}}_n\right]\end{array}$$

Each layer ${\mathbb{V}}_{n+1}$ contains all values from the previous layer ${\mathbb{V}}_n$, plus all bags, lists, and records formed from those values.

Definition (Value Domain). The set of all values is the union of all layers:

$$\mathbb{V}:=\bigcup _{n\in \mathbb{N}}{\mathbb{V}}_n$$

Theorem (Fixed Point). $\mathbb{V}$ satisfies the equation:

$$\mathbb{V}=\mathbb{Q}\bigsqcup \mathcal{B}\left(\mathbb{V}\right)\bigsqcup {\mathbb{V}}^{\ast }\bigsqcup \left[\mathcal{L}{\stackrel{}{\rightharpoonup }}_{\mathrm{fin}}\mathbb{V}\right]$$

Proof sketch.

• ($\supseteq$): Numbers are in ${\mathbb{V}}_0\subseteq \mathbb{V}$. Any bag, list, or record over $\mathbb{V}$ involves finitely many values, all lying in some layer ${\mathbb{V}}_N$. Thus it belongs to ${\mathbb{V}}_{N+1}\subseteq \mathbb{V}$.
• ($\subseteq$): By induction, each ${\mathbb{V}}_n\subseteq \mathbb{Q}\bigsqcup \mathcal{B}\left(\mathbb{V}\right)\bigsqcup {\mathbb{V}}^{\ast }\bigsqcup \left[\mathcal{L}{\stackrel{}{\rightharpoonup }}_{\mathrm{fin}}\mathbb{V}\right]$, so their union $\mathbb{V}$ is contained in the right-hand side. ∎

Theorem (Well-Foundedness). Every value $v\in \mathbb{V}$ has a unique minimal layer $\ell (v)\in \mathbb{N}$, the least $n$ such that $v\in {\mathbb{V}}_n$. If $v$ is a compound value (bag, list, or record), all its immediate constituents have strictly smaller layer: $\ell (\text{constituent})<\ell (v)$.

This ensures the axiom of regularity: there are no infinite descending chains of membership.

Models

Model Part

A model part assigns labels to data, thereby describing the data’s meaning. Formally, we define a model part as a function into $\mathcal{T}$ whose domain is a non-empty, finite set of labels. We denote the set of all model parts $\mathcal{M}$.

$$\mathcal{M}:=\{L\to \mathcal{T}\mid L\subset \mathcal{L}\wedge |L|\in {\mathbb{N}}^{+}\}$$

Type System

Overview

A type system classifies values into types, enabling static reasoning about program behavior. In our metamodel, types are defined as subsets of the value domain $\mathbb{V}$, and subtyping is derived from set inclusion.

Type Syntax

We define the set of types $\mathcal{T}$ inductively as the smallest set closed under the following constructors:

$$\begin{array}{rl}\mathcal{T}:=& \mathtt{Num}\mid \mathtt{Int}\mid \mathtt{T}(v)\mid \mathtt{Bag}(\mathcal{T})\mid \mathtt{List}(\mathcal{T},\mathcal{T})\\ & \mid \mathtt{Cons}(\mathcal{T},\mathcal{T})\mid \mathtt{Record}(l_1\mapsto \mathcal{T},\dots ,l_n\mapsto \mathcal{T})\mid \mathtt{ClosedRecord}(l_1\mapsto \mathcal{T},\dots ,l_n\mapsto \mathcal{T})\\ & \mid [a,b{]}_{{\text{incl}}_1,{\text{incl}}_2}\mid \mathtt{Mult}(\mathcal{T},\mathcal{T})\\ & \mid \mathcal{T}\cup \mathcal{T}\mid \mathcal{T}\cap \mathcal{T}\mid \mathcal{T}\setminus \mathcal{T}\\ & \mid \mu \alpha .\mathcal{T}\mid \mu ({\alpha }_1,\dots ,{\alpha }_n).({\tau }_1,\dots ,{\tau }_n)\end{array}$$

where:

• $v\in \mathbb{V}$
• $l_1,\dots ,l_n\in \mathcal{L}$ are distinct labels
• $a,b\in \mathbb{Q}\cup \{-\mathrm{\infty },+\mathrm{\infty }\}$
• ${\text{incl}}_1,{\text{incl}}_2\in \{\text{open},\text{closed}\}$
• $\alpha ,{\alpha }_1,\dots ,{\alpha }_n$ are type variables
• ${\tau }_1,\dots ,{\tau }_n$ are types that may reference the bound type variables

Primitive Types

• $\mathtt{Num}$: All rational numbers, $[[\mathtt{Num}]]=\mathbb{Q}$
• $\mathtt{Int}$: All integers, $[[\mathtt{Int}]]=\mathbb{Z}$

Singleton Types

For each value $v\in \mathbb{V}$, the singleton type $\mathtt{T}(v)$ contains exactly that value:

$$[[\mathtt{T}(v)]]=\{v\}$$

Parameterized Types

Bag type: $\mathtt{Bag}(T)$ represents bags where every element conforms to type $T$:

$$[[\mathtt{Bag}(T)]]=\mathcal{B}([[T]])$$

List type: $\mathtt{List}(T,L)$ represents lists where every element conforms to type $T$ and the length belongs to type $L$:

$$[[\mathtt{List}(T,L)]]=\{l\in {\mathbb{V}}^{\ast }\mid \mathrm{\forall }i\in \{0,\dots ,|l|-1\}.l[i]\in [[T]]\wedge |l|\in [[L]]\}$$

where $L$ is a type representing non-negative integers (e.g., an interval type).

Record type: $\mathtt{Record}(l_1\mapsto T_1,\dots ,l_n\mapsto T_n)$ represents open records with specified key types:

$$[[\mathtt{Record}(l_1\mapsto T_1,\dots ,l_n\mapsto T_n)]]=\{r\in \left[\mathcal{L}{\stackrel{}{\rightharpoonup }}_{\mathrm{fin}}\mathbb{V}\right]\mid \mathrm{\forall }i\in \{1,\dots ,n\}.r(l_i)\in [[T_i]]\}$$

Open records support width subtyping: a record with additional keys is a subtype.

Closed record type: $\mathtt{ClosedRecord}(l_1\mapsto T_1,\dots ,l_n\mapsto T_n)$ represents records with exactly the specified keys:

$$[[\mathtt{ClosedRecord}(l_1\mapsto T_1,\dots ,l_n\mapsto T_n)]]=\{r\in \left[\mathcal{L}{\stackrel{}{\rightharpoonup }}_{\mathrm{fin}}\mathbb{V}\right]\mid \text{dom}(r)=\{l_1,\dots ,l_n\}\wedge \mathrm{\forall }i\in \{1,\dots ,n\}.r(l_i)\in [[T_i]]\}$$

Sequence Types

Cons type: $\mathtt{Cons}(A,B)$ represents the concatenation of two sequence types:

$$[[\mathtt{Cons}(A,B)]]=\{\text{concat}(a,b)\mid a\in [[A]]\wedge b\in [[B]]\}$$

This constructor requires that $A$ and $B$ are sequence types (bags or lists). The concatenation operation $\text{concat}$ is defined for compatible sequence kinds.

Interval Types

Interval types represent subsets of $\mathbb{Q}$ bounded by rational numbers or infinity:

$$[[[a,b{]}_{{\text{incl}}_1,{\text{incl}}_2}]]=\{q\in \mathbb{Q}\mid a\le q\le b\}$$

with the constraint that inclusive bounds must be finite: if ${\text{incl}}_1=\text{closed}$, then $a\in \mathbb{Q}$; if ${\text{incl}}_2=\text{closed}$, then $b\in \mathbb{Q}$.

Notation: $[a,b]$ for both closed, $(a,b)$ for both open, $[a,b)$ for left closed and right open, $(a,b]$ for left open and right closed.

Numeric Types

Multiplication type: $\mathtt{Mult}(A,B)$ represents the set of all products of values from $A$ and $B$:

$$[[\mathtt{Mult}(A,B)]]=\{a\times b\mid a\in [[A]]\wedge b\in [[B]]\}$$

This constructor requires that $A$ and $B$ are numeric types (subtypes of $\mathtt{Num}$).

Set Operations

Union: $T_1\cup T_2$ represents the union of two types:

$$[[T_1\cup T_2]]=[[T_1]]\cup [[T_2]]$$

Intersection: $T_1\cap T_2$ represents the intersection of two types:

$$[[T_1\cap T_2]]=[[T_1]]\cap [[T_2]]$$

Set difference: $T_1\setminus T_2$ represents the set difference:

$$[[T_1\setminus T_2]]=[[T_1]]\setminus [[T_2]]$$

Recursive Types

Single Recursive Types

A recursive type $\mu \alpha .\tau$ binds a type variable $\alpha$ within the body $\tau$, allowing $\tau$ to reference the type being defined.

Semantics: The semantic function maps recursive types to the least fixed point of a recursive equation:

$$[[\mu \alpha .\tau ]]=\text{lfp}(X\mapsto [[\tau [X/\alpha ]]])$$

where $\text{lfp}$ denotes the least fixed point, and $\tau [X/\alpha ]$ denotes substitution of $X$ for $\alpha$ in $\tau$.

Example: A tree type:

$$\text{Tree}=\mu \alpha .\mathtt{Record}(\mathtt{value}\mapsto \mathtt{Int},\mathtt{children}\mapsto \mathtt{Bag}(\alpha ))$$

The semantic equation is:

$$X=\{r\in \left[\mathcal{L}{\stackrel{}{\rightharpoonup }}_{\mathrm{fin}}\mathbb{V}\right]\mid r(\mathtt{value})\in \mathbb{Z}\wedge r(\mathtt{children})\in \mathcal{B}\left(X\right)\}$$

The least fixed point is the set of all finite trees with integer values.

Base cases: A recursive type is inhabited if and only if its semantic equation has a non-empty least fixed point. This requires the type to have base cases that allow the recursion to terminate with finite, well-founded values.

Example (inhabited): $\mu \alpha .\mathtt{Record}(\mathtt{child}\mapsto \alpha \cup \mathtt{T}(\text{null}))$ has base case $\text{null}$, so it's inhabited by all finite chains ending in $\text{null}$.

Example (uninhabited): $\mu \alpha .\mathtt{Record}(\mathtt{child}\mapsto \alpha )$ has no base case, so its least fixed point is $\mathrm{\varnothing }$.

Mutually Recursive Types

Mutually recursive types are defined as a simultaneous fixed point of multiple type equations:

$$\mu ({\alpha }_1,\dots ,{\alpha }_n).({\tau }_1,\dots ,{\tau }_n)$$

Semantics: The semantic function maps this to the least fixed point of the system of equations:

$$[[\mu ({\alpha }_1,\dots ,{\alpha }_n).({\tau }_1,\dots ,{\tau }_n)]]=\text{lfp}((X_1,\dots ,X_n)\mapsto ([[{\tau }_1[\overrightarrow{X}/\overrightarrow{\alpha }]]],\dots ,[[{\tau }_n[\overrightarrow{X}/\overrightarrow{\alpha }]]]))$$

Example: Doubly-linked list nodes:

$$\mu (\alpha ,\beta ).(\mathtt{Record}(\mathtt{value}\mapsto \mathtt{Int},\mathtt{next}\mapsto \beta \cup \mathtt{T}(\text{null})),\mathtt{Record}(\mathtt{value}\mapsto \mathtt{Int},\mathtt{prev}\mapsto \alpha \cup \mathtt{T}(\text{null})))$$

This defines two types $\alpha$ and $\beta$ that reference each other.

Subtyping

Subtyping is derived from set inclusion of the semantic function:

$$T_1\le T_2⟺[[T_1]]\subseteq [[T_2]]$$

Examples:

• $\mathtt{Int}\le \mathtt{Num}$ because $\mathbb{Z}\subseteq \mathbb{Q}$
• $\mathtt{T}(42)\le \mathtt{Int}$ because $\{42\}\subseteq \mathbb{Z}$
• $\mathtt{Record}(\mathtt{a}\mapsto \mathtt{Int},\mathtt{b}\mapsto \text{tstring})\le \mathtt{Record}(\mathtt{a}\mapsto \mathtt{Int})$ (width subtyping for open records)
• $\mathtt{Int}\cup \text{tstring}\le \mathtt{Num}\cup \text{tstring}$ because $\mathbb{Z}\cup \mathbb{S}\subseteq \mathbb{Q}\cup \mathbb{S}$

Type Equivalence

Two types are equivalent if they have the same semantics:

$$T_1\equiv T_2⟺[[T_1]]=[[T_2]]$$

Typing Relation

A value $v$ has type $T$ if and only if $v$ belongs to the semantic interpretation of $T$:

$$v:T⟺v\in [[T]]$$