update

Author: RIvance

docs/04-overloading.md

@@ -42,11 +42,30 @@ This rule governs the application of overloaded functions. If a function `f` has
 #### Subtyping for Superposition Types
 
 $$
-(A \sqcup B) <: (A \oplus B)
+(A \oplus B) \leq (A \sqcap B)
 $$
 
-This rule states that a sum type $A \sqcup B$, which represents an exclusive choice between `A` and `B`, is a subtype of the corresponding superposition type $A \oplus B$. Superposition types provide more flexibility, allowing the function’s behavior to be dynamically resolved based on the context.
+The superposition type $A \oplus B$ is a subtype of the intersection type $A \sqcap B$.
+This rule comes from the property of an intersection type:
 
+$$
+(A_1 \to B_1) \sqcap (A_2 \to B_2) \equiv (A_1 \sqcup A_2) \to (B_1 \sqcap B_2)
+$$
+
+A superposition type $(A_1 \to B_1) \sqcap (A_2 \to B_2)$ yields $B_1$ when applied to $A_1$ and $B_2$ when applied to $A_2$. The input type satisfies $A_1 \geq A_1 \sqcup A_2$ and $A_2 \geq A_1 \sqcup A_2$, and the output type satisfies $B_1 \leq B_1 \sqcap B_2$ and $B_2 \leq B_1 \sqcap B_2$.
+And because the covariance of the input type and the contravariance of the output type:
+
+$$
+\begin{align}
+\begin{array}{c}
+\Gamma \vdash A_1 \geq B_1 \quad A_2 \leq B_2
+\\\hline
+\Gamma \vdash A_1 \rightarrow A_2 \leq B_1 \rightarrow B_2
+\end{array}
+\end{align}
+$$
+
+Thus, the superposition type is considered as a subtype of the intersection type.
 
 ## Function Application with Overloading
 
@@ -182,8 +201,6 @@ eval concat "Hello! "
 
 Here, `concat` can be partially applied to an integer or string, with its final behavior determined by the type of the subsequent argument. Specifically, applying an overloaded lambda to an argument invokes a selection process based on the argument’s type, identifying the corresponding function branch. This type-based selection mechanism is termed "**measurement**" of an overloaded lambda, analogous to quantum state measurement, where an indeterminate superposed state collapses into a definite outcome upon observation.
 
-
-
 ### Why Superposition Types?
 
 Superposition types in **Saki** elegantly combine **function overloading** (ad-hoc polymorphism) with **currying**, overcoming challenges that typically arise when attempting to integrate these concepts in functional programming languages.

docs/05-subtyping.md

@@ -10,6 +10,18 @@ $$
 \forall T, \ T \leq \top \quad \text{and} \quad  \forall T, \ \bot \leq 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 \leq B \quad \Gamma \vdash e : A}{\Gamma \vdash 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 \leq B \)), then we can treat \( e \) as an expression of type \( B \) without any further checks.
+
 ## Basic Subtype Relationships
 
 ### Reflexivity of Subtyping
@@ -239,138 +251,107 @@ For example:
 
 
 
+## Subtyping for Recursive Type
 
-
-
+$$
+\frac{
+\Gamma \vdash T : \mathcal{U} \quad \Gamma, x : T \vdash \sigma \leq T
+}{
+\Gamma \vdash \mu (x : T) . \sigma \leq 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.
 
-### Intersection of Dependent \( \Pi \)-Types
+### Subtyping Relationships
 
-#### Type Formation Rule for Intersection of Dependent \( \Pi \)-Types
+#### Dependent $\Pi$-Type
 
-Dependent \( \Pi \)-types are function-like types where the codomain depends on the specific value of the domain. For the intersection of such types:
+The dependent $\Pi$-type rule for subtyping is given by:
 
 $$
 \frac{
-\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}
+\Gamma \vdash A_2 \leq A_1 \quad \Gamma, x:A_1 \vdash B_1(x) \quad \Gamma, x:A_2 \vdash B_1(x) \leq B_2(x)
 }{
-\Gamma \vdash \Pi(x:A_1). B_1(x) \cap \Pi(x:A_2). B_2(x) : \mathcal{U}
+\Gamma \vdash \Pi(x:A_1). B_1(x) \leq \Pi(x:A_2). B_2(x)
 }
 $$
 
-Refinement ensures that \( x \) must be in both \( A_1 \) and \( A_2 \), producing:
+#### Dependent $\Sigma$-Type
+
+The dependent $\Sigma$-type rule for subtyping is given by:
 
 $$
 \frac{
-\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}
+\Gamma \vdash A_1 \leq A_2 \quad \Gamma, x:A_1 \vdash B_1(x) \leq B_2(x)
 }{
-\Gamma \vdash \Pi(x:A). B(x) : \mathcal{U}
+\Gamma \vdash \Sigma(x:A_1). B_1(x) \leq \Sigma(x:A_2). B_2(x)
 }
 $$
 
-#### Subtyping Rule for Intersection of Dependent \( \Pi \)-Types
+### Intersection of Dependent \( \Pi \)-Types
+
+#### Type Formation Rule for Intersection of Dependent \( \Pi \)-Types
 
-Subtyping for dependent \( \Pi \)-types follows:
+Dependent \( \Pi \)-types are function-like types where the codomain depends on the specific value of the domain. For the intersection of such types:
 
 $$
 \frac{
-\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)
+\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}
 }{
-\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)
+\Gamma \vdash \Pi(x:A_1). B_1(x) \cap \Pi(x:A_2). B_2(x) : \mathcal{U}
 }
 $$
 
-### Union of Dependent \( \Pi \)-Types
-
-#### Type Formation Rule for Union of Dependent \( \Pi \)-Types
-
-For unions of dependent \( \Pi \)-types, a sum type representation is used:
-
-$$
-\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))
-$$
-
-Where \( \text{inl} \) and \( \text{inr} \) represent injections into the left and right components.
-
-#### Typing Rule
-
-A term \( f \) of either constituent type satisfies:
+Refinement ensures that \( x \) must be in both \( A_1 \) and \( A_2 \), producing:
 
 $$
 \frac{
-\Gamma \vdash f : \Pi(x : A_1). B_1(x)
-}{
-\Gamma \vdash f : \Pi(x : A_1). B_1(x) \cup \Pi(x : A_2). B_2(x)
-}
-\quad \text{or} \quad
-\frac{
-\Gamma \vdash f : \Pi(x : A_2). B_2(x)
+\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}
 }{
-\Gamma \vdash f : \Pi(x : A_1). B_1(x) \cup \Pi(x : A_2). B_2(x)
+\Gamma \vdash \Pi(x:A). B(x) : \mathcal{U}
 }
 $$
 
-#### Subtyping Rule for Union of Dependent \( \Pi \)-Types
+#### Type Formation Rule for Intersection of Dependent \( \Sigma \)-Types
 
-Subtyping ensures inclusion and equivalence between unions and their constituents:
+Dependent \( \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{
-\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)
+\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}
 }{
-\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)
+\Gamma \vdash \Sigma(x:A_1). B_1(x) \cap \Sigma(x:A_2). B_2(x) : \mathcal{U}
 }
 $$
 
-A similar rule applies for the second component of the union.
-
-### Intersection of Dependent \( \Sigma \)-Types
-
-#### Type Formation Rule for Intersection of Dependent \( \Sigma \)-Types
-
-For dependent \( \Sigma \)-types, intersections represent the set of pairs satisfying constraints for both components:
-
-$$
-\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))
-$$
+### Union of Dependent \( \Pi \)-Types
 
-#### Subtyping Rule for Intersection of Dependent \( \Sigma \)-Types
+#### Type Formation Rule for Union of Dependent \( \Pi \)-Types
 
-The subtyping rule for intersected \( \Sigma \)-types is:
+The union of dependent \( \Pi \)-types combines the domains and codomains of the respective types:
 
 $$
 \frac{
-\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)
+\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}
 }{
-\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)
+\Gamma \vdash \Pi(x:A_1). B_1(x) \cup \Pi(x:A_2). B_2(x) : \mathcal{U}
 }
 $$
 
-### Union of Dependent \( \Sigma \)-Types
-
 #### Type Formation Rule for Union of Dependent \( \Sigma \)-Types
 
-Unions of dependent \( \Sigma \)-types follow a sum-type structure:
-
-$$
-\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))
-$$
-
-Here, \( \text{inl} \) and \( \text{inr} \) designate the left and right components.
-
-#### Typing Rule
-
-Subtyping for unions of \( \Sigma \)-types maintains compatibility:
+The union of dependent \( \Sigma \)-types combines the types of the first and second components:
 
 $$
 \frac{
-\Gamma \vdash (a, b) : \Sigma(x : A_1). B_1(x)
+\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}
 }{
-\Gamma \vdash (a, b) : \Sigma(x : A_1). B_1(x) \cup \Sigma(x : A_2). B_2(x)
+\Gamma \vdash \Sigma(x:A_1). B_1(x) \cup \Sigma(x:A_2). B_2(x) : \mathcal{U}
 }
 $$
+

docs/examples/hello.saki

@@ -0,0 +1 @@
+eval "Hello, world!"