docs: fix render errors

Author: RIvance

docs/Definition/Decorator.md

@@ -1,4 +1,4 @@
-## Decorator
+# Decorator
 
 A **decorator** in **Saki** is a higher-order function that takes another function as its argument and returns a new function with the same type signature. Decorators allow for the dynamic augmentation of functions with additional functionality, enhancing the behavior of the original function without modifying its core logic. In essence, a decorator has the type:
 
@@ -10,7 +10,7 @@ This means it takes a function of type `T -> R` and returns a function of the sa
 
 Decorators in **Saki** can be applied directly to functions using a specific syntax. They enable modular code, where functionality can be extended in a reusable and composable manner.
 
-### Syntax
+## Syntax
 
 The syntax for applying one or more decorators to a function is as follows:
 
@@ -27,7 +27,7 @@ def func: T -> R
 
 - **`#[dec1, dec2, ..., decN]`**: Decorators are applied using a `#` followed by a list of decorators enclosed in square brackets. These decorators are applied to the function that follows.
 
-### Typing Rules
+## Typing Rules
 
 Decorators must preserve the type signature of the functions they are applied to. If a function `func` has type `T -> R`, and a decorator `dec` transforms it while maintaining the same type, the resulting decorated function also has type `T -> R`. The typing rule can be formalized as:
 
@@ -37,61 +37,61 @@ $$
 
 This ensures that the decorator takes in a function of type `T -> R` and returns a function with the same signature.
 
-### Examples of Decorators
+## Examples
 
-1. **Ensuring Positive Input Values**
+### Ensuring Positive Input Values
 
-   Consider a decorator that ensures that a function only operates on positive input values. This decorator checks if the input is greater than 0 and only calls the original function if the condition is satisfied. Otherwise, it returns `None`.
+Consider a decorator that ensures that a function only operates on positive input values. This decorator checks if the input is greater than 0 and only calls the original function if the condition is satisfied. Otherwise, it returns `None`.
 
-   ```scala
-   universe GreaterThan(T: 'Type) = contract {
-       require (>)(self, other: T): Bool
-   }
+```scala
+universe GreaterThan(T: 'Type) = contract {
+    require (>)(self, other: T): Bool
+}
 
-   def ensurePositive[T: 'GreaterThan(ℕ)](func: T -> Option[T]): T -> Option[T] = {
-       return |arg: T|: Option[T] => if arg > 0 then func(arg) else None
-   }
+def ensurePositive[T: 'GreaterThan(ℕ)](func: T -> Option[T]): T -> Option[T] = {
+    return |arg: T|: Option[T] => if arg > 0 then func(arg) else None
+}
 
-   #[ensurePositive]
-   def safeDivide(x: ℕ): Option[ℕ] = if x != 0 then Some(10 / x) else None
-   ```
+#[ensurePositive]
+def safeDivide(x: ℕ): Option[ℕ] = if x != 0 then Some(10 / x) else None
+```
 
-   - **`ensurePositive`**: The decorator checks if the input is greater than 0. If true, it calls the original function; otherwise, it returns `None`.
-   - **`safeDivide`**: This function divides 10 by the input value, but using the decorator, it is guaranteed to only operate on positive integers. If the input is 0 or negative, it returns `None`.
+- **`ensurePositive`**: The decorator checks if the input is greater than 0. If true, it calls the original function; otherwise, it returns `None`.
+- **`safeDivide`**: This function divides 10 by the input value, but using the decorator, it is guaranteed to only operate on positive integers. If the input is 0 or negative, it returns `None`.
 
-2. **Transforming Input Before Applying a Function**
+### Transforming Input Before Applying a Function
 
-   The following example demonstrates how a decorator can be used to modify the input before passing it to the original function.
+The following example demonstrates how a decorator can be used to modify the input before passing it to the original function.
 
-   ```scala
-   def mapInput[T1 T2 R: 'Type](transform: T1 -> T2, func: T2 -> R): T1 -> R = {
-       return |arg: T1|: R => func(transform(arg))
-   }
+```scala
+def mapInput[T1 T2 R: 'Type](transform: T1 -> T2, func: T2 -> R): T1 -> R = {
+    return |arg: T1|: R => func(transform(arg))
+}
 
-   #[mapInput(|x: ℕ| => x * 2)]
-   def half(n: ℕ): ℕ = n / 2
-   ```
+#[mapInput(|x: ℕ| => x * 2)]
+def half(n: ℕ): ℕ = n / 2
+```
 
-   - **`mapInput`**: This decorator takes a transformation function and applies it to the input before passing it to the original function.
-   - **`half`**: This function divides the input by 2, but with the decorator applied, the input is first doubled, so `half(5)` would return the result of `10 / 2`, which is `5`.
+- **`mapInput`**: This decorator takes a transformation function and applies it to the input before passing it to the original function.
+- **`half`**: This function divides the input by 2, but with the decorator applied, the input is first doubled, so `half(5)` would return the result of `10 / 2`, which is `5`.
 
-3. **Transforming the Output of a Function**
+### Transforming the Output of a Function
 
-   A decorator can also be used to modify the output of a function. In the following example, the decorator multiplies the function's result by 10.
+A decorator can also be used to modify the output of a function. In the following example, the decorator multiplies the function's result by 10.
 
-   ```scala
-   def mapOutput[T R1 R2: 'Type](func: T -> R1, transform: R1 -> R2): T -> R2 = {
-       return |arg: T|: R2 => transform(func(arg))
-   }
-   
-   #[mapOutput(|x: ℕ| => x * 10)]
-   def increment(n: ℕ): ℕ = n + 1
-   ```
+```scala
+def mapOutput[T R1 R2: 'Type](func: T -> R1, transform: R1 -> R2): T -> R2 = {
+    return |arg: T|: R2 => transform(func(arg))
+}
+
+#[mapOutput(|x: ℕ| => x * 10)]
+def increment(n: ℕ): ℕ = n + 1
+```
 
-   - **`mapOutput`**: This decorator takes a transformation function and applies it to the output of the original function.
-   - **`increment`**: This function adds 1 to the input, but with the decorator, the result is multiplied by 10. So, `increment(5)` results in `60`, as `(5 + 1) * 10 = 60`.
+- **`mapOutput`**: This decorator takes a transformation function and applies it to the output of the original function.
+- **`increment`**: This function adds 1 to the input, but with the decorator, the result is multiplied by 10. So, `increment(5)` results in `60`, as `(5 + 1) * 10 = 60`.
 
-### Composition of Decorators
+## Composition of Decorators
 
 Decorators in Saki can be composed. Multiple decorators can be applied to the same function in sequence. This means that each decorator applies its transformation on the function that results from the previous decorator.
 
@@ -108,7 +108,7 @@ In this case:
 
 If the input to `safeDivideAndScale` is `2`, the function returns `Some(50)` (since `10 / 2 = 5` and `5 * 10 = 50`). If the input is `0`, the function returns `None` due to `ensurePositive`.
 
-#### Contract Universes and Decorators
+### Contract Universes and Decorators
 
 In Saki, decorators can leverage **contract universes** to enforce behavior through constraints. For example, decorators like `ensurePositive` can depend on contract universes such as `'GreaterThan`, ensuring that the function operates only on types that support comparison.
 

docs/Definition/Function Overloading.md

@@ -0,0 +1,102 @@
+# Function Overloading
+
+In **Saki**, function overloading is introduced by leveraging a new type construct called the **superposition type** ($A \oplus B$), which allows a single function to operate over multiple input types, providing different behaviors based on the types of arguments passed to the function. This generalizes traditional function overloading, often found in programming languages, into the type-theoretic framework of **Martin-Löf Type Theory (MLTT)**. The superposition type formalizes this behavior, ensuring that function overloading is type-safe and rigorous, enabling polymorphism at the type level.
+
+## Superposition Types
+
+The **superposition type** $A \oplus B$ encapsulates the ability of a function to accept multiple types as input and return different types depending on the context of the application. Unlike a **sum type** ($A \sqcup B$), which restricts a term to belong to either $A$ or $B$, the superposition type dynamically resolves the term’s type based on the argument passed, making it applicable multiple times for different types.
+
+For example, if a function can handle both integer and string types, its type would be expressed as $Int \oplus String$, meaning that the function can accept either type, and the appropriate behavior will be applied based on the argument.
+
+### Typing Rules for Superposition Types
+
+The rules for superposition types enable the safe typing and application of overloaded functions in the type system. These rules are as follows:
+
+1. **Term Typing for Superposition Types**:
+
+$$
+\frac{\Gamma \vdash t: A \quad \Delta \vdash t: B}{\Gamma, \Delta \vdash t: A \oplus B}
+$$
+
+If a term $t$ can be typed as both $A$ in context $\Gamma$ and $B$ in context $\Delta$, then $t$ can be assigned the superposition type $A \oplus B$ in the combined context $\Gamma, \Delta$. This allows the function to behave polymorphically, with its type determined by the argument.
+
+2. **Function Overloading with Superposition**:
+
+$$
+\frac{\Gamma \vdash t: A \rightarrow B \quad \Delta \vdash t: A \rightarrow C}{\Gamma, \Delta \vdash t: A \rightarrow (B \oplus C)}
+$$
+
+This rule allows a function to have multiple return types based on the context of its application. The function `t` can return either `B` in context $\Gamma$ or `C$ in context $\Delta$, and the final type is resolved as $B \oplus C$ depending on the argument.
+
+3. **Function Application for Overloaded Functions**:
+
+$$
+\frac{\Gamma \vdash f: (A \rightarrow B) \oplus (C \rightarrow D) \quad \Gamma \vdash t: A}{\Gamma \vdash f\ t: B}
+$$
+
+This rule governs the application of overloaded functions. If a function `f` has a superposition type $(A \rightarrow B) \oplus (C \rightarrow D)$, applying it to an argument of type `A` resolves the function to return type `B`.
+
+4. **Subtyping for Superposition Types**:
+
+$$
+(A \sqcup B) <: (A \oplus 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.
+
+## Example of Function Overloading with Superposition
+
+Consider the following example where a function `f` can take either an integer or a string as input and perform different operations:
+
+```scala
+def f(x: Int): Int = x + 1
+def f(x: String): String = x + "!"
+```
+
+In **Saki**, this behavior would be captured by a superposition type:
+
+```scala
+f: (Int -> Int) ⊕ (String -> String)
+```
+
+When called with an integer, `f(5)` returns `6`; when called with a string, `f("Hello")` returns `"Hello!"`.
+
+### Overloading via `let-in` Expressions
+
+The **`let-in` expression** in Saki can also incorporate superposition types, allowing for function overloading in local contexts. The general form of the `let-in` expression is:
+
+$$
+\text{let } x = t_1 \text{ in } t_2
+$$
+
+If `t_1` has a superposition type, the variable `x` inherits this type, and the body `t_2` must handle each possible type that `x` may take on.
+
+#### Typing Rule for Overloaded `let-in`
+
+$$
+\frac{\Gamma \vdash t_1 : A \oplus C \quad \Gamma, x:A \vdash t_2 : B \quad \Gamma, x:C \vdash t_2 : D}{\Gamma \vdash \text{let } x = t_1 \text{ in } t_2 : B \oplus D}
+$$
+
+In this case:
+
+- $t_1$ has the superposition type $A \oplus C$.
+- $t_2$ is well-typed under both contexts $\Gamma, x:A$ and $\Gamma, x:C$, producing types $B$ and $D$.
+- The resulting type of the `let-in` expression is $B \oplus D$, reflecting the dynamic resolution based on the branch of the superposition.
+
+#### Function Overloading in Context
+
+In **Saki**, overloaded functions may operate on different types, but their behavior and return type must be well-typed in each case. For example, consider the following overloaded function `g`:
+
+```scala
+def g(x: Int): String = "The number is " + x.toString
+def g(x: Bool): String = if x then "True" else "False"
+```
+
+The type of `g` would be:
+
+```scala
+g: (Int -> String) ⊕ (Bool -> String)
+```
+
+When `g` is applied to an integer, it returns a string representing the number; when applied to a boolean, it returns `"True"` or `"False"`.
+