Continuing fixes

Author: Nxirda

doc/glossary/containers.hpp

@@ -3,10 +3,40 @@
 
 @page containers Container Types
 
-## Container Type (Type Constructors)
-A **Container Type** is a **Type Constructor**; it is not a type itself but a function that takes a type \f$ T \f$ and returns a new type \f$ F(T) \f$.
+@section container_type Container Type (Type Constructors)
+A **Container Type** is not a type itself, but a **Type Constructor**: a function that takes a type \f$ T \f$ and 
+returns a new type \f$ F(T) \f$.
 
-* **Generics:** In C++, these are implemented via Templates.
-* **Structure:** It defines the "shape" of the data (e.g., `std::vector`, `std::list`) independently of the contained value.
+---
+
+@section type_constructor The Role of F(T)
+
+While Product and Sum types compose existing types, a Container defines a "shape" or "structure" independently of the 
+data it holds.
+
+* **Generics**: In C++, these are implemented via Templates. The template `std::vector<T>` is the constructor; 
+                `std::vector<int>` is the resulting type.
+
+* **Transformation**: Containers often allow for "Mapping" (Functors), where a function \f$ A \to B \f$ can be lifted 
+                      to transform \f$ F(A) \to F(B) \f$.
+
+@subsection container_programming Programming Languages Considerations
+
+In the context of **Kumi**, understanding the difference between the **Container** (the wrapper) and the **Product** 
+(the contents) is vital for optimization.
+
+| Container Concept | C++ Implementation | Algebraic Intuition |
+|:------------------|:-------------------|:--------------------|
+| List / Sequence   | `std::vector<T>`   | Ordered collection of \f$ T \f$ |
+| Set               | `std::set<T>`      | Unique collection of \f$ T \f$ |
+
+### Example
+```cpp
+template<typename T>
+struct Box {
+    T value; // Box is the Type Constructor F
+};
+
+Box<int> instance; // F(int)
 
 **/

doc/glossary/identities.hpp

@@ -3,48 +3,57 @@
 
 @page identity The Identity Elements (The "0" and "1" of Types)
 
-@tableofcontents
-
-* Just as there are neutral elements for the different mathematical operations, there are neutral elements for types. 
-With this said, before building complex types, we must define the identities that govern type algebra. 
-These types are the foundational "identity" elements.
+Just as there are neutral elements for mathematical operations, there are neutral elements for types. The neutral is a 
+mathematical element that has no effect on the computation such that using it results in the identity. The  simplest 
+example might be adding 0 to some natural number. With this said, before building complex types, we must define the 
+neutrals that govern type algebra. These types are the foundational "identity" elements.
 
 ---
 
 @section empty Empty Type : \f$ (0 / \bot) \f$
 
-The **Empty Type** is the identity element for **Sums** \f$ (A + 0 \cong A ) \f$.
+The **Empty Type** is the identity element for **Sums** \f$ (A + 0 \cong A ) \f$. It represents a type with no 
+inhabitants.
+
 * **Cardinality**: 0 states. It is mathematically impossible to construct an instance of this type.
-* **Algebraic Role**: In logic, it represents a contradiction. In code, it represents a path that can never be taken. 
+
+* **Algebraic Role**: In logic, it represents a contradiction. In code, it represents a path that can never be reached. 
                       A function returning the Empty Type is a "diverging" function (it never returns).
+
 * **Identity Property**:  Just as \f$ x + 0 = x \f$, having a choice between Type A or an impossible Type 0 is logically 
                           equivalent to simply having Type A.
 
 One cannot write such a type, but could specify a function that returns empty, in C++ this can be expressed the 
 following way.
 ```cpp
-[[noreturn]] void foo(){ }
+[[noreturn]] void foo() { 
+  throw std:runtime_error("Never returns");
+}
 ```
 
 ---
 
 @section unit Unit Type : \f$ (1 / \top) \f$
 
-The **Unit Type** is the identity element for **Products** \f$ (A \times 1 \cong A) \f$.
-Also refered to as the product of no types.
+The **Unit Type** is the identity element for **Products** \f$ (A \times 1 \cong A) \f$. It represents a type with
+exactly one inhabitant.
+
+@note It is also refered to as the product of no types.
 
 * **Cardinality**: 1 state. It contains exactly one possible value (often written as `()`).
+
 * **Algebraic Role**: It represents "no information" or "success without data." Because there is only one possible state, 
                       the value itself is predictable and thus carries zero entropy.
+
 * **Identity Property**:  Just as \f$ x \times 1 = x \f$, a pair containing Type A and a Unit Type provides no more 
                           information than Type A alone.
 
-In C++ such a type can be written simply as a singleton.
+In C++ such a type can be written simply as an empty struct. 
 ```cpp
 struct unit {};
 ```
 
-[In the next page](@ref product), we will see how to combine these simple types in order to compose what we call 
-product types which is the main topic of kumi.
+[In the next page](@ref product), we will see how to combine the simple types we saw until now in order to create more 
+complex types.
 
 **/

doc/glossary/introduction.hpp

@@ -4,19 +4,22 @@
 @page introduction Type Theoretic Foundations
 
 This introduction does not aim at providing full understanding of type theory, but is more focused on giving a brief yet
-extensive overview of the basis that might be of interest to any new or even experienced programmer. Kumi makes extensive
-use of some concepts that will be detailed in the following sections.
+extensive overview of the basis that might be of interest to any new or even experienced programmer. **Kumi** makes 
+extensive use of some concepts that will be detailed in the following sections. In the current state, the **Kumi** 
+library focuses on handling [product types](@ref product_type).
+
+---
 
 @section origin Origin 
 
-**Type Theory** is the academic study of type systems used to formalize how types are constructed and composed. 
+Type theory is the academic study of type systems used to formalize how types are constructed and composed. 
 While Set Theory categorizes elements into sets, Type Theory categorizes data (propositions) and the transformations 
 (proofs) applied to them.
 
 In this view:
 
-* **Types** are classifications of data (propositions).
-* **Functions/Programs** are the logical steps that transform data (proofs).
++ **Types** are classifications of data (propositions).
++ **Functions/Programs** are the logical steps that transform data (proofs).
 
 ---
 
@@ -26,14 +29,14 @@ The **Curry-Howard Correspondence** formalizes the direct link between logical r
 Every concept in logic has a direct counter part in type theory.
 The following table recapitulates the different operation that can be necessary to understand.
 
-| Logic Name    | Logic Notation      | Type Notation       | Type Name              | C++ Example             |
-| :------------ | :-------------------| :-------------------| :----------------------| :-----------------------|
-| True          | \f$ \top      \f$   | \f$ \top       \f$  | Unit Type              | `std::monostate`        |
-| False         | \f$ \bot      \f$   | \f$ \bot       \f$  | Empty Type             | `void`                  |
-| Implication   | \f$ A \to B   \f$   | \f$ A \to B    \f$  | Function               | `std::function<B(A)>`   |
-| Not           | \f$ \neg A    \f$   | \f$ A \to 0    \f$  | Function to empty type | `[[noreturn]] void foo` |
-| And           | \f$ A \land B \f$   | \f$ A \times B \f$  | Product type           | `std::tuple<A,B>`       |
-| Or            | \f$ A \lor B  \f$   | \f$ A + B      \f$  | Sum type               | `std::variant<A,B>`     |
+| Logic Name    | Logic Notation      | Type Notation       | Type Name              | C++ Example                  |
+| :------------ | :-------------------| :-------------------| :----------------------|:-----------------------------|
+| True          | \f$ \top      \f$   | \f$ \top       \f$  | Unit Type              | `std::monostate`             |
+| False         | \f$ \bot      \f$   | \f$ \bot       \f$  | Empty Type             | `void` (as a non-return type)|
+| Implication   | \f$ A \to B   \f$   | \f$ A \to B    \f$  | Function               | `std::function<B(A)>`        |
+| Not           | \f$ \neg A    \f$   | \f$ A \to 0    \f$  | Function to empty type | `[[noreturn]] void foo`      |
+| And           | \f$ A \land B \f$   | \f$ A \times B \f$  | Product type           | `std::tuple<A,B>`            |
+| Or            | \f$ A \lor B  \f$   | \f$ A + B      \f$  | Sum type               | `std::variant<A,B>`          |
 
 ---
 
@@ -52,11 +55,29 @@ x : bool      // A formal variable
 Then in order to be able to manipulate these types, there is the concept of functions terms. This is simply a function 
 in the programming sens. Given a parameter of a type \f$ \sigma \f$ and a return type \f$ \tau \f$ the associated function
 is noted \f$ \sigma \rightarrow \tau \f$. The addition of two real numbers can then written as : 
-\f$ add : *nat* \rightarrow (*nat* \rightarrow *nat*)\f$
+add : nat \f$ \rightarrow \f$ (nat \f$ \rightarrow \f$ nat)
 
 Finally, there are lambda terms, it is associated to concept of anonymous functions/lambdas functions in programming, 
 these should sound familiar. They simply represent a way to define new function terms. 
 
+---
+
+@section cardinality Type Cardinality
+
+In the context of Set Theory, the **Cardinality** of a set is simply the number of element it contains. When translating
+it to Type THeory, the cardinality of a type refers to the total number of unique values (or states) an instance of that 
+type can possibly represent.
+
+By treating types as set of potential values, we can use standard arithmetic to predict the complexity of our data 
+structuresr:
+
+* **Finite Sets**: A type like ```bool``` as a cardinality of 2, the set of it's values is \f$ {true, false} \f$
+
+* **The Power of Counting**: Understanding cardinality allows us to see types not just as labels, but as mathematical
+                            objects where the size of the state space dictates how much information a variable can have.
+
+---
+
 [In the next page](@ref identity), we will see some more specific types that are used as a base for more complex 
 operations.
 

doc/glossary/product.hpp

@@ -3,15 +3,15 @@
 
 @page product Product Types 
 
-@tableofcontents
-
 @section product_construction Product Constructions (The Logic of "AND")
 
 Products represent types where multiple elements exist simultaneously.
 The operands of the product are types. 
 The structure of a product type is determined by the fixed order of the operands. 
 
-@subsection product_type Product Type \f$ (A \times B) \f$
+---
+
+@section product_type Product Type \f$ (A \times B) \f$
 
 A **Product Type** is a compound type formed by combining multiple types. 
 
@@ -46,36 +46,70 @@ A product type follows **List Algebra**.
 + **Order Dependence**: Position is identity. \f$ (A, B) \f$ is structurally distinct from \f$ (B, A) \f$ even though they contain the same underlying types.
 + **Cardinality**: The total state space is the **product** of the states of its components: \f$ Card(A \times B) = Card(A) \times Card(B) \f$.
 
-### Example
-```cpp
-std::tuple<int, float> p; // Ordered product
-```
+@subsection tuple_programming Programming Languages Considerations 
 
-@note A pair is a special case of a tuple that is composed of only two elements.
+Product types can also be composed of homogeneous types, such a tuple does not differ from array types. In most programming
+models homogeneous product types can be efficiently stored via contiguous location in memory without needing to insert 
+padding. By definition, an homogeneous product type can be iterated on by indexing as the gap between two consecutive 
+elements is fixed. This property does not hold for their heterogeneous counterpart
 
-* **Reference** [Wikipedia: Tuple](https://en.wikipedia.org/wiki/Tuple)
+The C++ standard library provides an implementation of a tuple type as well as some special cases. Kumi provides a generic
+yet optimized representation of them. Each type provided in the standard can be represented efficiently.
+
+| STL type            | Kumi                    |
+|:--------------------|:------------------------|
+| std::pair<T1,T2>;   | kumi::tuple<T1,T2>      |
+| std::tuple<Ts...>;  | kumi::tuple<Ts...>      |
+| std::array<T,5>;    | kumi::tuple<T,T,T,T,T>  |
+| std::complex<T>;    | kumi::tuple<T,T>        |
 
 ---
 
-@subsection record_type Record Type \f$ \{label: Type\} \f$  (The Struct)
+@section record_type Record Type \f$ \{label: Type\} \f$  (The Struct)
 
 A **Record Type** identifies its components by a **unique label** rather than a position. 
 
 An instance of a record type is called a struct in many programming languages.
 (Let aside considerations about object oriented progamming, inheritance, etc...)
 
 A **Record Type** is the labeled version of a Product, it can be seen as the product of mathematical sets. 
+Similarily to tuples, it accepts one constructor that takes a variadic number of input that are in this case fields.
+
+Formally it can be written as :
+
+\f$ \{l_1 : x_1, l_2 : x_2, ..., l_n : x_n\} : T_1 x T_2 x ... x T_n \f$
+
+This can be read as : the record is composed of elements of types \f$ T_1 \f$ to \f$ T_n\f$
+with corresponding values \f$ x_1 \f$ to \f$ x_n \f$ that are labeled with \f$ l_1 to l_n \f$.
+
+The corresponding definition in kumi could look like the following:
+```cpp
+using namespace kumi::literals;
+kumi::record a = { "x"_id = 42, "y"_id = 13.37f, "z"_id = 'd' };
+```
+
+To extract values from a record, there are projections that are term constructors.
+A projection (often noted \f$ \pi \f$) is a function that given a product type 
+returns the elements. Formally it is denoted as : 
+
+\f$ \pi_1(x) : T_1, \pi_2(x) : T_2, ..., \pi_n(x) : T_n \f$
+
+In kumi this corresponds to the `get` functions
+```c
+auto a = kumi::get<"x">(kumi::record{ "x"_id = 42, "y"_id = 13.37f, "z"_id = 'd' });
+```
+
 It follows **Set Algebra** on top of **List Algebra**.
++ **Label Identity**: Components are identified by unique **Labels** (names) rather than position.
++ **Permutation**:  Theoretically, a record is a set of field mappings. In many formal definitions, `{x: int, y: float}` 
+                    is isomorphic to `{y: float, x: int}` because the set of labels and their associated types are identical.
++ **Semantic Access**: Access is performed via labels (`u.id`), adding semantic meaning to the structure.
 
 Operation on records are traditionally not structural in the sens that they operate per label, never per 
 element. However, as they are internally represented by a tuple, such operation are permitted. As an example, one
 could "rotate" a record \f$ n \f$ positions to the left. Mathematically this might not make a lot of sens
 whereas for a programmer that has to consider memory representation, this is potentially critical to have.
 
-+ **Label Identity**: Components are identified by unique **Labels** (names) rather than position.
-+ **Permutation**:  Theoretically, a record is a set of field mappings. In many formal definitions, `{x: int, y: float}` 
-                    is isomorphic to `{y: float, x: int}` because the set of labels and their associated types are identical.
-+ **Semantic Access**: Access is performed via labels (`u.id`), adding semantic meaning to the structure.
 
 ### Example 
 ```cpp
@@ -84,9 +118,13 @@ struct User {
     float score;  // Label: score
 };
 ```
-
-* **Reference** [Wikipedia: Record](https://en.wikipedia.org/wiki/Record_(computer_science))
+---
 
 [In the next page](@ref sum), we will see the duals of product types which are called sum types.
 
+---
+
+* **Reference** [Wikipedia: Tuple](https://en.wikipedia.org/wiki/Tuple)
+* **Reference** [Wikipedia: Record](https://en.wikipedia.org/wiki/Record_(computer_science))
+
 **/

doc/glossary/sum.hpp

@@ -3,28 +3,42 @@
 
 @page sum Sum Types 
 
-@tableofcontents
-
 @section sum_construction Sum Constructions (The Logic of "OR")
 
-Sums represent types where a choice is made between different alternatives. They are the mathematical **Dual** of Products.
+Sums represent types where a choice is made between different alternatives. They are the mathematical **Dual** of 
+Products Types.
 
 @subsection sum_type Sum Type  \f$ (A + B) \f$ (The Coproduct)
 
 An unlabeled, positional choice between types. 
+
+An instance of a sum type represents an **Exclusive Choice**, formally it is the disjoint union of sets.
+
 * **Exclusive Choice**: An instance of \f$ A + B \f$ contains either an A or a B, but never both simultaneously.
+
 * **Cardinality**: The state space is the **sum** of its components: \f$ Card(A + B) = Card(A) + Card(B) \f$.
+
 * **Algebraic Property**: It is the dual of the Product. While a Product asks you to "Take All," a Sum asks you to "Pick One."
 
+In C++, this is most commonly represented by `std::variant`.
 ### Example
 ```cpp
 std::variant<int, float> p; 
 ```
 
-@subsection variant Variant (The Labeled Sum)
-A **Variant** is the labeled version of a Sum Type (and thus the dual of the Record).
-* **Active Labeling**: Just as a Record has multiple labels present at once, a Variant has exactly **one active label** from a set of possibilities.
-* **The Tag**: In C++, `std::variant` implements this as a **Tagged Union**. It uses a small integer (the tag/index) to track which label is currently active, ensuring type safety.
+---
+
+@section variant Variant Type (The Labeled Sum)
+
+A **Variant** (commonly refered to as Tagged Union) is the labeled version of a Sum Type, serving as the dual of the 
+**Record**.
+
+While a Record has multiple labels present at once, a Variant as exactly one active label from a set of possibilities.
+
+* **The Tag**: To ensure type safety, the implementation often uses a tag to track the currently stored type.
+
+* **Cardinality**: The state space of a variant is the sum of the cardinalities of it's fields:
+                    \f$ Card({l_1 : T_1, l_2 : T_2, ..., l_n : T_n}) = \sum_i^n Card(T_i) \f$
 
 ### Example 
 ```cpp
@@ -35,4 +49,12 @@ union particles {
 };
 ```
 
+@note As of today, kumi does not provides it's own sum types. The focus was made on product type and it's associated 
+algebra.
+
+---
+
+[In the next page](@ref containers), we will one of the last kind of types that can be found througout kumi which are 
+called container types.
+
 **/

doc/layout.xml

@@ -14,6 +14,7 @@
         <tab type="user" url="@ref identity" title="Identity Types"/>
         <tab type="user" url="@ref product" title="Product Types"/>
         <tab type="user" url="@ref sum" title="Sum Types"/>
+        <tab type="user" url="@ref containers" title="Container Types"/>
       </tab>
       <tab type="user" url="@ref cpp_spec" title="C++ Vocabulary"/>
       <tab type="user" url="@ref nomenclature" title="Nomenclature"/>