docs: update

Author: RIvance

docs/03-proofs.md

@@ -131,7 +131,7 @@ We begin by establishing the formal definitions of equality, reflexivity, and sy
 The equality relation between two elements $a, b$ of a type $A$ is defined as a dependent type $A.Eq(a, b)$, which asserts that $a$ and $b$ are equal. This is expressed using a dependent type $A \to \mathcal{U}$ where $\mathcal{U}$ is the universe of types. Formally, the equality type $A.Eq(a, b)$ is defined as:
 
 $$
-A.Eq(a, b) :\equiv \forall P : (A \to \mathcal{U}), P(a) \to P(b)
+Eq_A(a, b) :\equiv \forall (P : A \to \mathcal{U}) . P(a) \to P(b)
 $$
 
 This means that $A.Eq(a, b)$ holds if, for all propositions $P$ on $A$, whenever $P(a)$ is true, $P(b)$ must also hold. In essence, this defines equality as the ability to substitute $a$ for $b$ in any context described by $P$.
@@ -150,17 +150,15 @@ The property of **reflexivity** asserts that any element $a$ of a type $A$ is eq
 For any element $a \in A$, reflexivity is stated as:
 
 $$
-A.Eq(a, a) :\equiv \forall P : (A \to \mathcal{U}), P(a) \to P(a)
+\text{refl}_A : \forall(a: A) . Eq_A(a, a) :\equiv \lambda (P : A \to \mathcal{U}) . \lambda (p : P(a)) . p
 $$
 
 This is trivially true because the proof $pa : P(a)$ already holds. Reflexivity is defined as:
 
 <div class="code-editor">
 
 ```
-def refl(A: 'Type, a: A): A.Eq(a, a) = {
-    (P: A -> 'Type, pa: P(a)) => pa
-}
+def refl(A: 'Type, a: A): A.Eq(a, a) = (P: A -> 'Type, p: P(a)) => p
 ```
 </div>
 
@@ -173,7 +171,10 @@ The property of **symmetry** states that if $a = b$, then $b = a$. Formally, giv
 The symmetry of equality is defined as follows:
 
 $$
-A.Eq(b, a) :\equiv \forall P : (A \to \mathcal{U}), P(b) \to P(a)
+\begin{align}
+\text{symm}_A : & \, \forall(a, b: A) . Eq_A(a, b) \to Eq_A(b, a) 
+    \\ & :\equiv \lambda (e_{ab} : Eq_A(a, b)) . e_{ab}(\lambda (b' : A) . Eq_A(b', a), \text{refl}_A(a))
+\end{align}
 $$
 
 Given a proof of $A.Eq(a, b)$, we construct a proof of $A.Eq(b, a)$ by applying $A.Eq(a, b)$ to the proposition $P(b') = A.Eq(b', a)$, and using the reflexivity of $a$. This is formally stated as:

docs/Definition/Function Overloading.md docs/Definition/01-overloading.mddocs/Definition/Function Overloading.md renamed to docs/Definition/01-overloading.md

@@ -1,5 +1,8 @@
 # Decorator
 
+!!! warning
+    This feature is not yet implemented or not fully supported in the current version of Saki interpreter/REPL.
+
 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:
 
 $$

docs/Definition/Decorator.md docs/Definition/02-decorator.mddocs/Definition/Decorator.md renamed to docs/Definition/02-decorator.md

@@ -1,3 +1,8 @@
+# Expressions
+
+<script type="module" src="/javascripts/editor.js"></script>
+<link rel="stylesheet" href="/static/styles.css">
+
 ## If Expression Terms
 
 The **if-expression** in **Saki** provides a way to perform conditional branching, allowing a program to execute one of two expressions based on a boolean condition. Unlike some languages where control flow statements are separate from expressions, Saki’s **if-expression** integrates into the language's expression system, meaning that an **if-expression** always evaluates to a value.
@@ -23,10 +28,25 @@ $$
 \frac{\Gamma \vdash t_1: \mathbb{B} \quad \Gamma \vdash t_2: T \quad \Gamma \vdash t_3: T}{\Gamma \vdash \text{if } t_1 \text{ then } t_2 \text{ else } t_3 : T}
 $$
 
-This rule states that:
+Where:
+
 - The condition $t_1$ must have type `Bool` (denoted by $\mathbb{B}$).
 - The `then` and `else` branches ($t_2$ and $t_3$) must both have the same type $T$ for the if-expression to be well-typed.
 
+<div class="code-editor" id="code-if">
+
+```
+eval {
+    let value = 10
+    if value % 2 == 0 then "Even" else "Odd"
+}
+```
+</div>
+<div class="button-container">
+    <button class="md-button button-run" onclick="runCodeInEditor('code-if', 'result-if')">Run Code</button>
+</div>
+<div class="result-editor" id="result-if"></div>
+
 
 ## Match Expression Terms
 
@@ -56,39 +76,58 @@ $$
 \frac{\Gamma \vdash t: T \quad \Gamma \vdash p_i: T \quad \Gamma \vdash e_i: R}{\Gamma \vdash \text{match } t \ \{ \ p_1 \Rightarrow e_1 \mid \dots \mid p_n \Rightarrow e_n \ \} : R}
 $$
 
-This means that:
-- The term being matched (`t`) must have type `T`.
-- Each pattern `p_i` must match against the type `T`.
-- The expression `e_i` associated with each pattern must have the same result type `R`.
-- The patterns must be exhaustive, meaning that all possible forms of the term are covered by the patterns.
+Where:
 
-### Examples
+- The term $t$ being matched must have type $T$.
+- Each pattern $p_i$ must correspond to a value of type $T$.
+- The expression $e_i$ associated with each pattern must return the same type $R$, ensuring uniformity across all branches.
+- The patterns must be exhaustive, covering all possible values of the term $t$. Failing to provide exhaustive patterns would result in a type error, as not all possible values would be handled.
 
-#### Pattern Matching on Algebraic Data Types
+### Example: Boolean Pattern Matching
 
-Consider the `Option` type:
+In the following example, a boolean value is matched against two patterns: `true` and `false`:
 
-```scala
-def getValue[A: 'Type](opt: Option[A], default: A): A = match opt {
-    case Option[A]::Some(x) => x
-    case Option[A]::None => default
+<div class="code-editor" id="code-match-bool">
+
+```
+def toInt(b: Bool): ℤ = match b {
+    case true => 1
+    case false => 0
 }
+
+eval true.toInt  // Result: 1
+eval false.toInt // Result: 0
 ```
+</div>
+<div class="button-container">
+    <button class="md-button button-run" onclick="runCodeInEditor('code-match-bool', 'result-match-bool')">Run Code</button>
+</div>
+<div class="result-editor" id="result-match-bool"></div>
 
-- This function takes an `Option[A]` and a default value.
-- If the option is `Some(x)`, it returns `x`; if it is `None`, it returns the default value.
+Here, the match-expression transforms a boolean value into an integer representation by explicitly handling both possible cases of a `Bool` type.
 
-#### Exhaustive Matching
+### Pattern Matching on Inductive Types
 
-Match expressions must cover all possible cases for the type being matched. For example, when matching on `Bool`:
+Pattern matching becomes particularly useful when working with inductive types, which may represent optional values, lists, or other recursively defined structures. Consider the following inductive type `Option`:
+
+<div class="code-editor" id="code-match-option">
 
-```scala
-def toInt(b: Bool): ℤ = match b with {
-    case true => 1
-    case false => 0
-}
 ```
+type Option[A: 'Type] = inductive {
+    None
+    Some(A)
+}
 
-- This function converts a `Bool` value to an integer.
-- Both possible values (`true` and `false`) are covered, making the pattern match exhaustive.
+def getOrDefault[A: 'Type](opt: Option[A], default: A): A = match opt {
+    case Option[A]::Some(x) => x
+    case Option[A]::None => default
+}
 
+eval Option[Int]::Some(114514).getOrDefault[Int](0) // Result: 114514
+eval Option[Int]::None.getOrDefault[Int](0)         // Result: 0
+```
+</div>
+<div class="button-container">
+    <button class="md-button button-run" onclick="runCodeInEditor('code-match-option', 'result-match-option')">Run Code</button>
+</div>
+<div class="result-editor" id="result-match-option"></div>

docs/Terms/Function (Lambda).md docs/Terms/01-lambda.mddocs/Terms/Function (Lambda).md renamed to docs/Terms/01-lambda.md

@@ -0,0 +1,132 @@
+# Algebraic Datatype
+
+<script type="module" src="/javascripts/editor.js"></script>
+<link rel="stylesheet" href="/static/styles.css">
+
+**Algebraic Datatype (ADT)** is a special kind of inductive types that are essential in functional programming and type theory. They are used to define composite types by combining other types using **sum types** (also known as **variants**) and **product types**. ADTs are particularly useful for modeling data that can take multiple distinct forms, and they are foundational in expressing complex structures such as trees, lists, and option types. In **Saki**, ADTs are defined using the `enum` keyword and can be parameterized by types and type classes, with the ability to incorporate contract universes for constrained types.
+
+## Syntax of Algebraic Datatypes
+
+The syntax for defining ADTs in Saki follows a straightforward pattern:
+
+```
+InductiveCons     ::= Ident (‘(’ Term (‘,’ Term)* ‘)’)?
+InductiveTypeTerm ::= ‘inductive’ ‘{’ InductiveCons (‘,’ InductiveCons)* ‘}’
+```
+
+- **EnumCons**: Represents each constructor of the algebraic datatype. A constructor can either be a simple identifier (like `None`) or an identifier with parameters (like `Some(A)`).
+- **EnumTypeTerm**: The ADT is introduced using the `inductive` keyword, followed by a list of constructors enclosed in braces `{}`. Multiple constructors can be defined, separated by commas.
+
+Each constructor defines a specific form that a value of the ADT can take, either as a simple tag or as a combination of different types. ADTs in Saki resemble **sum types** in type theory, where each constructor defines a possible variant of the type.
+
+Algebraic Data Types can be understood as **sum types** in type theory, which are defined using **coproducts**. A sum type, like `A + B`, represents a type that can hold either a value of type `A` or a value of type `B`. In the context of ADTs:
+- Each constructor of the ADT corresponds to an inclusion map into the coproduct.
+- The ADT represents the **disjoint union** of its constructors.
+
+For instance, the type `Option(A)` is defined as:
+$$
+\text{Option}(A) \cong 1 + A
+$$
+Where:
+
+- `1` represents the `None` constructor (the unit type), indicating absence.
+- `A` represents the `Some` constructor, indicating presence.
+
+Similarly, the tree type `Tree[A]` can be seen as:
+$$
+\text{Tree}(A) \cong 1 + (\text{Color} \times A \times \text{Tree}(A) \times \text{Tree}(A))
+$$
+This reflects the two possible forms of the tree:
+
+- A `Leaf` (represented by `1`).
+- A `Node`, which holds a `Color`, a value of type `A`, and two subtrees of type `Tree[A]`.
+
+## Examples of ADTs in Saki
+
+### Simple Algebraic Data Type: `Color`
+
+The following is an example of a simple ADT called `Color`, which represents a type with no parameters and has two distinct values: `Red` and `Black`.
+
+<div class="code-editor">
+
+```
+type Color = inductive { Red; Black }
+```
+</div>
+
+In this case, `Color` is a sum type with two possible values, `Red` and `Black`. Each constructor defines a unique value of the `Color` type. This is a basic example of an ADT, where no additional parameters or data are required.
+
+### Parameterized Algebraic Data Type: `Option`
+
+The `Option` type is a more complex example of an ADT. It represents a type that can either contain a value of type `A` or no value at all.
+
+<div class="code-editor">
+
+```
+type Option(A: 'Type) = inductive {
+    None
+    Some(A)
+}
+```
+</div>
+
+- **`Option(A)`**: A generic ADT parameterized by a type `A`.
+- **`None`**: A constructor representing the absence of a value.
+- **`Some(A)`**: A constructor representing the presence of a value of type `A`.
+
+
+### Nested Algebraic Data Type: `List`
+
+The following example illustrates a recursive ADT that defines a list structure. The `List` type is parameterized by a type `A` and has two constructors: `Nil`, representing an empty list, and `Cons`, which constructs a new list by prepending an element of type `A` to an existing list of type `List[A]`.
+
+<div class="code-editor">
+
+```
+type List[A: 'Type] = inductive {
+    Nil
+    Cons(A, List[A])
+}
+```
+</div>
+
+- **`Nil`**: Represents an empty list.
+- **`Cons(A, List[A])`**: Represents a non-empty list, where the first element is of type `A` and the rest is a list of type `List[A]`.
+
+### Tree Structure Using ADTs: `Tree`
+
+The following example defines a binary tree structure, where each node contains a color, a value of type `A`, and two subtrees of the same type `Tree[A]`.
+
+<div class="code-editor">
+
+```
+type Tree[A: 'Type] = inductive {
+    Leaf
+    Node(Color, A, Tree[A], Tree[A])
+}
+```
+</div>
+
+- **`Leaf`**: Represents a leaf node, which has no data.
+- **`Node(Color, A, Tree[A], Tree[A])`**: Represents an internal node that contains a value of type `A`, a `Color`, and two subtrees of type `Tree[A]`.
+
+
+## ADT/Inductive Constructor Access
+
+In Saki, the constructors of inductive types (including ADTs) can be accessed using the `::` operator. For example:
+
+<div class="code-editor" id="code-adt-constructor-access">
+
+```
+type Option(A: 'Type) = inductive {
+    None
+    Some(A)
+}
+
+eval Option(Int)::None
+eval Option(String)::Some
+```
+</div>
+<div class="button-container">
+    <button class="md-button button-run" onclick="runCodeInEditor('code-adt-constructor-access', 'result-adt-constructor-access')">Run Code</button>
+</div>
+<div class="result-editor" id="result-adt-constructor-access"></div>