Subtyping and Algebraic Subtyping

Subtyping is mathematically represented as a subset relation, $A\subseteq B$, such that $\mathrm{\forall }t\in A,t\in B$. This interpretation allows subtyping to reflect a preorder relation, which becomes a partial order under equivalence ($A\le B\wedge B\le A⟹A=B$). The introduction of least upper bounds (lub, $A\bigsqcup B$) and greatest lower bounds (glb, $A\sqcap B$) converts this structure into a lattice. When combined with the universal top type ($\mathrm{\top }$) and bottom type ($\mathrm{\perp }$), the lattice becomes bounded, satisfying:

$$\mathrm{\forall }T,T\le \mathrm{\top }\text{and}\mathrm{\forall }T,\mathrm{\perp }\le T$$

The Subsumption Rule

In a type system with subtyping, a type $A$ can be considered a subtype of another type $B$ if $A$ satisfies all the constraints and properties of $B$, and possibly some additional ones. The subsumption rule formalizes this idea by allowing expressions of a more specific type to be treated as expressions of a more general type.

The subsumption rule can be expressed as:

$$\frac{A\le B\mathrm{\Gamma }⊢e:A}{\mathrm{\Gamma }⊢e:B}$$

This means that if we have an expression $e$ of type $A$, and we know that $A$ is a subtype of $B$ (denoted $A\le B$), then we can treat $e$ as an expression of type $B$ without any further checks.

Basic Subtype Relationships

Reflexivity of Subtyping

Subtyping is reflexive, implying any type $T$ is trivially a subtype of itself:

$$\begin{array}{r}\begin{array}{c}\\ T\le T\end{array}\end{array}$$

This property is foundational to any preorder relation that subtyping models.

Transitivity of Subtyping

Transitivity guarantees consistency across multiple subtyping relations. If $T_1\le T_2$ and $T_2\le T_3$, then $T_1\le T_3$. Formally:

$$\begin{array}{r}\begin{array}{c}\mathrm{\Gamma }⊢T_1\le T_2\mathrm{\Gamma }⊢T_2\le T_3\\ \mathrm{\Gamma }⊢T_1\le T_3\end{array}\end{array}$$

Functions

The subtyping relation for function types follows contravariant behavior in the parameter type and covariant behavior in the return type:

$$\begin{array}{r}\begin{array}{c}\mathrm{\Gamma }⊢A_1\ge B_1{A}_2\le B_2\\ \mathrm{\Gamma }⊢A_1\to A_2\le B_1\to B_2\end{array}\end{array}$$

Here, $A_1\ge B_1$ indicates the parameter type $A_1$ is a supertype of $B_1$, while $A_2\le B_2$ requires the return type $A_2$ to be a subtype of $B_2$.

Union and Intersection Types

Union Types

Union types, denoted $\bigsqcup$, allow combining types such that a value of the union type belongs to at least one constituent type:

$$\begin{array}{r}\begin{array}{c}\mathrm{\forall }i.\mathrm{\exists }j.(\mathrm{\Gamma }⊢A_i\le B_j)\\ \mathrm{\Gamma }⊢\underset{i}{⨆}{A}_i\le \underset{j}{⨆}{B}_j\end{array}\end{array}$$

This expresses that the union of subtypes remains a subtype of the union of their respective supertypes.

Intersection Types

Intersection types, denoted $\sqcap$, describe a type that belongs simultaneously to multiple constituent types:

$$\begin{array}{r}\begin{array}{c}\mathrm{\Gamma }⊢\mathrm{\forall }i.\mathrm{\exists }j.(A_i\ge B_j)\\ \mathrm{\Gamma }⊢{⨅}_i{A}_i\ge {⨅}_j{B}_j\end{array}\end{array}$$

The intersection of supertypes forms a supertype of the intersection of their respective subtypes.

Relationships

For function types, union and intersection obey distributive laws:

$$(A_1\to B_1)\sqcap (A_2\to B_2)=(A_1\bigsqcup A_2)\to (B_1\sqcap B_2)$$

This states that the intersection of function types corresponds to the union of parameter types and the intersection of return types.

For example:

(Int -> String) & (Float -> Bool)

Run Example

Similarly, the union of function types results from the intersection of parameter types and the union of return types.

$$(A_1\to B_1)\bigsqcup (A_2\to B_2)=(A_1\sqcap A_2)\to (B_1\bigsqcup B_2)$$

For example:

(Int -> String) | (Float -> Bool)

Run Example

Records

Subtyping for record types aligns with structural subtyping, where records are compatible if they share the same fields and types. The typing rule for record types is:

$$\begin{array}{r}\begin{array}{c}\mathrm{\Gamma }⊢{\overline{t_i:T_i}}^i\\ \mathrm{\Gamma }⊢\{{\overline{l_i=t_i}}^i\}:\{{\overline{l_i:T_i}}^i\}\end{array}\end{array}$$

Here, ${\overline{t_i:T_i}}^i$ denotes record fields, and field labels $l_i$ and types $T_i$ determine the record's type.

Field access ensures type preservation:

$$\begin{array}{r}\begin{array}{c}\mathrm{\Gamma }⊢t:\{{\overline{l_i:T_i}}^i\}\\ \mathrm{\Gamma }⊢t.l_i:T_i\end{array}\end{array}$$

Subtyping among records supports the subset relation:

$$\begin{array}{r}\begin{array}{c}\\ \mathrm{\forall }S.\mathrm{\forall }(S^{\prime }\subseteq S).(\{{\overline{l_i:T_i}}^{i\in S}\}\le \{{\overline{l_i:T_i}}^{i\in S^{\prime }}\})\end{array}\end{array}$$

If fields $S^{\prime }$ are a subset of $S$, then their respective record types exhibit a subtyping relationship.

Pointwise subtyping applies across all fields in records:

$$\begin{array}{r}\begin{array}{c}\mathrm{\Gamma }⊢\mathrm{\forall }i.(A_i\le B_i)\\ \mathrm{\Gamma }⊢\{{\overline{a_i:A_i}}^i\}\le \{{\overline{b_i:B_i}}^i\}\end{array}\end{array}$$

Union and Intersection Rules for Record Types

In algebraic subtyping, union ($\bigsqcup$) and intersection ($\sqcap$) types can also be extended to record types. These operations allow record subtyping to support partial and combined views of records, ensuring compatibility and flexibility in handling structured data.

Union of Record Types

The union of two record types combines their fields, allowing overlapping fields to resolve to the union of their respective types:

$$\{{\overline{l_i:A_i}}^{i\in S}\}\bigsqcup \{{\overline{l_i:B_i}}^{i\in T}\}=\{{\overline{l_i:A_i\bigsqcup B_i}}^{i\in S\cap T},{\overline{l_j:A_j}}^{j\in S\setminus T},{\overline{l_k:B_k}}^{k\in T\setminus S}\}$$

• For shared fields $l_i\in S\cap T$, the resulting type is the union of their individual types $A_i\bigsqcup B_i$.
• For fields exclusive to one record (e.g., $l_j\in S\setminus T$ or $l_k\in T\setminus S$), their types remain unchanged.

For example:

(record { a: Int; b: String }) | (record { b: Float; c: Bool })

Run Example

Intersection of Record Types

The intersection of two record types combines their fields similarly, but overlapping fields resolve to the intersection of their types:

$$\{{\overline{l_i:A_i}}^{i\in S}\}\sqcap \{{\overline{l_i:B_i}}^{i\in T}\}=\{{\overline{l_i:A_i\sqcap B_i}}^{i\in S\cap T}\}$$

• Only fields common to both records ($l_i\in S\cap T$) are preserved in the resulting record.
• For shared fields, the resulting type is the intersection of their individual types $A_i\sqcap B_i$.
• Fields exclusive to one record are excluded from the intersection.

For example:

(record { a: Int; b: String }) & (record { b: String; c: Bool })

Run Example

Subtyping for Recursive Type

$$\frac{\mathrm{\Gamma }⊢T:\mathcal{U}\mathrm{\Gamma },x:T⊢\sigma \le T}{\mathrm{\Gamma }⊢\mu (x:T).\sigma \le T}$$

Dependent Types

Dependent types extend the expressive power of type systems by allowing types to depend on values or other types. Algebraic subtyping supports dependent types, incorporating union and intersection constructs to define relationships between dependent types effectively.

Subtyping Relationships

Dependent $\mathrm{\Pi }$-Type

The dependent $\mathrm{\Pi }$-type rule for subtyping is given by:

$$\frac{\mathrm{\Gamma }⊢A_2\le A_1\mathrm{\Gamma },x:A_1⊢B_1(x)\mathrm{\Gamma },x:A_2⊢B_1(x)\le B_2(x)}{\mathrm{\Gamma }⊢\mathrm{\Pi }(x:A_1).B_1(x)\le \mathrm{\Pi }(x:A_2).B_2(x)}$$

Dependent $\mathrm{\Sigma }$-Type

The dependent $\mathrm{\Sigma }$-type rule for subtyping is given by:

$$\frac{\mathrm{\Gamma }⊢A_1\le A_2\mathrm{\Gamma },x:A_1⊢B_1(x)\le B_2(x)}{\mathrm{\Gamma }⊢\mathrm{\Sigma }(x:A_1).B_1(x)\le \mathrm{\Sigma }(x:A_2).B_2(x)}$$

Intersection of Dependent $\mathrm{\Pi }$-Types

Type Formation Rule for Intersection of Dependent $\mathrm{\Pi }$-Types

Dependent $\mathrm{\Pi }$-types are function-like types where the codomain depends on the specific value of the domain. For the intersection of such types:

$$\frac{\mathrm{\Gamma }⊢A_1:\mathcal{U}\mathrm{\Gamma }⊢A_2:\mathcal{U}\mathrm{\Gamma },x:A_1⊢B_1(x):\mathcal{U}\mathrm{\Gamma },x:A_2⊢B_2(x):\mathcal{U}}{\mathrm{\Gamma }⊢\mathrm{\Pi }(x:A_1).B_1(x)\cap \mathrm{\Pi }(x:A_2).B_2(x):\mathcal{U}}$$

Refinement ensures that $x$ must be in both $A_1$ and $A_2$, producing:

$$\frac{\mathrm{\Gamma }⊢A=A_1\cap A_2:\mathcal{U}\mathrm{\Gamma },x:A⊢B(x)=B_1(x)\cap B_2(x):\mathcal{U}}{\mathrm{\Gamma }⊢\mathrm{\Pi }(x:A).B(x):\mathcal{U}}$$

Type Formation Rule for Intersection of Dependent $\mathrm{\Sigma }$-Types

Dependent $\mathrm{\Sigma }$-types represent dependent pairs, where the type of the second component depends on the value of the first. The intersection of such types is defined as:

$$\frac{\mathrm{\Gamma }⊢A_1:\mathcal{U}\mathrm{\Gamma }⊢A_2:\mathcal{U}\mathrm{\Gamma },x:A_1⊢B_1(x):\mathcal{U}\mathrm{\Gamma },x:A_2⊢B_2(x):\mathcal{U}}{\mathrm{\Gamma }⊢\mathrm{\Sigma }(x:A_1).B_1(x)\cap \mathrm{\Sigma }(x:A_2).B_2(x):\mathcal{U}}$$

Union of Dependent $\mathrm{\Pi }$-Types

Type Formation Rule for Union of Dependent $\mathrm{\Pi }$-Types

The union of dependent $\mathrm{\Pi }$-types combines the domains and codomains of the respective types:

$$\frac{\mathrm{\Gamma }⊢A_1:\mathcal{U}\mathrm{\Gamma }⊢A_2:\mathcal{U}\mathrm{\Gamma },x:A_1⊢B_1(x):\mathcal{U}\mathrm{\Gamma },x:A_2⊢B_2(x):\mathcal{U}}{\mathrm{\Gamma }⊢\mathrm{\Pi }(x:A_1).B_1(x)\cup \mathrm{\Pi }(x:A_2).B_2(x):\mathcal{U}}$$

Type Formation Rule for Union of Dependent $\mathrm{\Sigma }$-Types

The union of dependent $\mathrm{\Sigma }$-types combines the types of the first and second components:

$$\frac{\mathrm{\Gamma }⊢A_1:\mathcal{U}\mathrm{\Gamma }⊢A_2:\mathcal{U}\mathrm{\Gamma },x:A_1⊢B_1(x):\mathcal{U}\mathrm{\Gamma },x:A_2⊢B_2(x):\mathcal{U}}{\mathrm{\Gamma }⊢\mathrm{\Sigma }(x:A_1).B_1(x)\cup \mathrm{\Sigma }(x:A_2).B_2(x):\mathcal{U}}$$