Skip to content

Commit 6905a46

Browse files
RIvanceRIvance
committed
subtyping
1 parent 3d6378f commit 6905a46

File tree

1 file changed

+296
-0
lines changed

1 file changed

+296
-0
lines changed

‎docs/05-subtyping.md‎

Lines changed: 296 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,296 @@
1+
2+
# Subtyping and Algebraic Subtyping
3+
4+
Subtyping is mathematically represented as a subset relation, \( A \subseteq B \), such that \( \forall t \in A, t \in B \). This interpretation allows subtyping to reflect a preorder relation, which becomes a partial order under equivalence (\( A \leq B \land B \leq A \implies A = B \)). The introduction of least upper bounds (lub, \( A \sqcup B \)) and greatest lower bounds (glb, \( A \sqcap B \)) converts this structure into a lattice. When combined with the universal top type (\( \top \)) and bottom type (\( \bot \)), the lattice becomes bounded, satisfying:
5+
6+
$$
7+
\forall T, \ T \leq \top \quad \text{and} \quad \forall T, \ \bot \leq T
8+
$$
9+
10+
## Basic Subtype Relationships
11+
12+
### Reflexivity of Subtyping
13+
Subtyping is reflexive, implying any type \( T \) is trivially a subtype of itself:
14+
15+
$$
16+
\begin{align}
17+
\begin{array}{c}
18+
\\\hline
19+
T \leq T
20+
\end{array}
21+
\end{align}
22+
$$
23+
24+
This property is foundational to any preorder relation that subtyping models.
25+
26+
### Transitivity of Subtyping
27+
Transitivity guarantees consistency across multiple subtyping relations. If \( T_1 \leq T_2 \) and \( T_2 \leq T_3 \), then \( T_1 \leq T_3 \). Formally:
28+
29+
$$
30+
\begin{align}
31+
\begin{array}{c}
32+
\Gamma \vdash T_1 \leq T_2 \quad \Gamma \vdash T_2 \leq T_3
33+
\\\hline
34+
\Gamma \vdash T_1 \leq T_3
35+
\end{array}
36+
\end{align}
37+
$$
38+
39+
## Functions
40+
The subtyping relation for function types follows contravariant behavior in the parameter type and covariant behavior in the return type:
41+
42+
$$
43+
\begin{align}
44+
\begin{array}{c}
45+
\Gamma \vdash A_1 \geq B_1 \quad A_2 \leq B_2
46+
\\\hline
47+
\Gamma \vdash A_1 \rightarrow A_2 \leq B_1 \rightarrow B_2
48+
\end{array}
49+
\end{align}
50+
$$
51+
52+
Here, \( A_1 \geq B_1 \) indicates the parameter type \( A_1 \) is a supertype of \( B_1 \), while \( A_2 \leq B_2 \) requires the return type \( A_2 \) to be a subtype of \( B_2 \).
53+
54+
## Union and Intersection Types
55+
56+
### Union Types
57+
Union types, denoted \( \sqcup \), allow combining types such that a value of the union type belongs to at least one constituent type:
58+
59+
$$
60+
\begin{align}
61+
\begin{array}{c}
62+
\forall i \,.\, \exists j \,.\, (\Gamma \vdash A_i \leq B_j)
63+
\\\hline
64+
\Gamma \vdash \bigsqcup_i A_i \leq \bigsqcup_j B_j
65+
\end{array}
66+
\end{align}
67+
$$
68+
69+
This expresses that the union of subtypes remains a subtype of the union of their respective supertypes.
70+
71+
### Intersection Types
72+
Intersection types, denoted \( \sqcap \), describe a type that belongs simultaneously to multiple constituent types:
73+
74+
$$
75+
\newcommand{\bigsqcap}{\mathop ⨅}
76+
\begin{align}
77+
\begin{array}{c}
78+
\Gamma \vdash \forall i \,.\, \exists j \,.\, (A_i \geq B_j)
79+
\\\hline
80+
\Gamma \vdash \bigsqcap_i A_i \geq \bigsqcap_j B_j
81+
\end{array}
82+
\end{align}
83+
$$
84+
85+
The intersection of supertypes forms a supertype of the intersection of their respective subtypes.
86+
87+
### Relationships
88+
For function types, union and intersection obey distributive laws:
89+
90+
$$
91+
(A_1 \to B_1) \sqcap (A_2 \to B_2) = (A_1 \sqcup A_2) \to (B_1 \sqcap B_2)
92+
$$
93+
94+
This states that the intersection of function types corresponds to the union of parameter types and the intersection of return types.
95+
96+
$$
97+
(A_1 \to B_1) \sqcup (A_2 \to B_2) = (A_1 \sqcap A_2) \to (B_1 \sqcup B_2)
98+
$$
99+
100+
Similarly, the union of function types results from the intersection of parameter types and the union of return types.
101+
102+
## Records
103+
Subtyping for record types aligns with structural subtyping, allowing more permissive views:
104+
105+
$$
106+
\begin{align}
107+
\begin{array}{c}
108+
\Gamma \vdash \overline{t_i : T_i}^i
109+
\\ \hline
110+
\Gamma \vdash \{ \overline{l_i = t_i}^i \} : \{ \overline{l_i : T_i}^i \}
111+
\end{array}
112+
\end{align}
113+
$$
114+
115+
Here, \( \overline{t_i : T_i}^i \) denotes record fields, and field labels \( l_i \) and types \( T_i \) determine the record's type.
116+
117+
Field access ensures type preservation:
118+
119+
$$
120+
\begin{align}
121+
\begin{array}{c}
122+
\Gamma \vdash t: \{ \overline{l_i : T_i}^i \}
123+
\\\hline
124+
\Gamma \vdash t.l_i : T_i
125+
\end{array}
126+
\end{align}
127+
$$
128+
129+
Subtyping among records supports the subset relation:
130+
131+
$$
132+
\begin{align}
133+
\begin{array}{c}
134+
\\\hline
135+
\forall S \,.\, \forall (S' \subseteq S) \,.\, (\{\overline{l_i : T_i}^{i \in S}\} \leq \{\overline{l_i : T_i}^{i \in S'}\})
136+
\end{array}
137+
\end{align}
138+
$$
139+
140+
If fields \( S' \) are a subset of \( S \), then their respective record types exhibit a subtyping relationship.
141+
142+
Pointwise subtyping applies across all fields in records:
143+
144+
$$
145+
\begin{align}
146+
\begin{array}{c}
147+
\Gamma \vdash \forall i \,.\, (A_i \leq B_i)
148+
\\\hline
149+
\Gamma \vdash \{\overline{a_i : A_i}^i\} \leq \{\overline{b_i : B_i}^i\}
150+
\end{array}
151+
\end{align}
152+
$$
153+
154+
155+
156+
157+
158+
159+
160+
161+
162+
163+
164+
165+
166+
167+
168+
## Dependent Types
169+
170+
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.
171+
172+
### Intersection of Dependent \( \Pi \)-Types
173+
174+
#### Type Formation Rule for Intersection of Dependent \( \Pi \)-Types
175+
176+
Dependent \( \Pi \)-types are function-like types where the codomain depends on the specific value of the domain. For the intersection of such types:
177+
178+
$$
179+
\frac{
180+
\Gamma \vdash A_1 : \mathcal{U} \quad \Gamma \vdash A_2 : \mathcal{U} \quad \Gamma, x:A_1 \vdash B_1(x) : \mathcal{U} \quad \Gamma, x:A_2 \vdash B_2(x) : \mathcal{U}
181+
}{
182+
\Gamma \vdash \Pi(x:A_1). B_1(x) \cap \Pi(x:A_2). B_2(x) : \mathcal{U}
183+
}
184+
$$
185+
186+
Refinement ensures that \( x \) must be in both \( A_1 \) and \( A_2 \), producing:
187+
188+
$$
189+
\frac{
190+
\Gamma \vdash A = A_1 \cap A_2 : \mathcal{U} \quad \Gamma, x:A \vdash B(x) = B_1(x) \cap B_2(x) : \mathcal{U}
191+
}{
192+
\Gamma \vdash \Pi(x:A). B(x) : \mathcal{U}
193+
}
194+
$$
195+
196+
#### Subtyping Rule for Intersection of Dependent \( \Pi \)-Types
197+
198+
Subtyping for dependent \( \Pi \)-types follows:
199+
200+
$$
201+
\frac{
202+
\Gamma \vdash A_2 \leq A_1 \quad \Gamma \vdash B_1(x) \leq B_2(x) \quad \Gamma \vdash B_2(x) \leq B_1(x)
203+
}{
204+
\Gamma \vdash \Pi(x : A_1). B_1(x) \cap \Pi(x : A_2). B_2(x) \leq \Pi(x : A_2). B_2(x)
205+
}
206+
$$
207+
208+
### Union of Dependent \( \Pi \)-Types
209+
210+
#### Type Formation Rule for Union of Dependent \( \Pi \)-Types
211+
212+
For unions of dependent \( \Pi \)-types, a sum type representation is used:
213+
214+
$$
215+
\Pi(x : A_1). B_1(x) \cup \Pi(x : A_2). B_2(x) \equiv \text{inl}(\Pi(x : A_1). B_1(x)) \cup \text{inr}(\Pi(x : A_2). B_2(x))
216+
$$
217+
218+
Where \( \text{inl} \) and \( \text{inr} \) represent injections into the left and right components.
219+
220+
#### Typing Rule
221+
222+
A term \( f \) of either constituent type satisfies:
223+
224+
$$
225+
\frac{
226+
\Gamma \vdash f : \Pi(x : A_1). B_1(x)
227+
}{
228+
\Gamma \vdash f : \Pi(x : A_1). B_1(x) \cup \Pi(x : A_2). B_2(x)
229+
}
230+
\quad \text{or} \quad
231+
\frac{
232+
\Gamma \vdash f : \Pi(x : A_2). B_2(x)
233+
}{
234+
\Gamma \vdash f : \Pi(x : A_1). B_1(x) \cup \Pi(x : A_2). B_2(x)
235+
}
236+
$$
237+
238+
#### Subtyping Rule for Union of Dependent \( \Pi \)-Types
239+
240+
Subtyping ensures inclusion and equivalence between unions and their constituents:
241+
242+
$$
243+
\frac{
244+
\Gamma \vdash \Pi(x : A_1). B_1(x) \leq \Pi(x : A_1). B_1(x) \cup \Pi(x : A_2). B_2(x)
245+
}{
246+
\Gamma \vdash \Pi(x : A_1). B_1(x) \cup \Pi(x : A_2). B_2(x) \leq \Pi(x : A_1). B_1(x)
247+
}
248+
$$
249+
250+
A similar rule applies for the second component of the union.
251+
252+
### Intersection of Dependent \( \Sigma \)-Types
253+
254+
#### Type Formation Rule for Intersection of Dependent \( \Sigma \)-Types
255+
256+
For dependent \( \Sigma \)-types, intersections represent the set of pairs satisfying constraints for both components:
257+
258+
$$
259+
\Sigma(x : A_1). B_1(x) \cap \Sigma(x : A_2). B_2(x) \equiv \Sigma(x : A_1 \cap A_2). (B_1(x) \cap B_2(x))
260+
$$
261+
262+
#### Subtyping Rule for Intersection of Dependent \( \Sigma \)-Types
263+
264+
The subtyping rule for intersected \( \Sigma \)-types is:
265+
266+
$$
267+
\frac{
268+
\Gamma \vdash A_2 \leq A_1 \quad \Gamma \vdash B_1(x) \leq B_2(x) \quad \Gamma \vdash B_2(x) \leq B_1(x)
269+
}{
270+
\Gamma \vdash \Sigma(x : A_1). B_1(x) \cap \Sigma(x : A_2). B_2(x) \leq \Sigma(x : A_2). B_2(x)
271+
}
272+
$$
273+
274+
### Union of Dependent \( \Sigma \)-Types
275+
276+
#### Type Formation Rule for Union of Dependent \( \Sigma \)-Types
277+
278+
Unions of dependent \( \Sigma \)-types follow a sum-type structure:
279+
280+
$$
281+
\Sigma(x : A_1). B_1(x) \cup \Sigma(x : A_2). B_2(x) \equiv \text{inl}(\Sigma(x : A_1). B_1(x)) \cup \text{inr}(\Sigma(x : A_2). B_2(x))
282+
$$
283+
284+
Here, \( \text{inl} \) and \( \text{inr} \) designate the left and right components.
285+
286+
#### Typing Rule
287+
288+
Subtyping for unions of \( \Sigma \)-types maintains compatibility:
289+
290+
$$
291+
\frac{
292+
\Gamma \vdash (a, b) : \Sigma(x : A_1). B_1(x)
293+
}{
294+
\Gamma \vdash (a, b) : \Sigma(x : A_1). B_1(x) \cup \Sigma(x : A_2). B_2(x)
295+
}
296+
$$

0 commit comments

Comments
 (0)