Skip to content

Commit 6fdec53

Browse files
NxirdaNxirda
committed
Reorganize per page with c++ format, easier to maintain
1 parent 3c406c3 commit 6fdec53

File tree

10 files changed

+279
-135
lines changed

10 files changed

+279
-135
lines changed

‎doc/glossary/containers.hpp‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#error This file is for documentation only - DO NOT INCLUDE
2+
/**
3+
4+
@page containers Container Types
5+
6+
## Container Type (Type Constructors)
7+
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$.
8+
9+
* **Generics:** In C++, these are implemented via Templates.
10+
* **Structure:** It defines the "shape" of the data (e.g., `std::vector`, `std::list`) independently of the contained value.
11+
12+
**/

doc/cpp_vocabulary.md renamed to doc/glossary/cpp_vocabulary.md

File renamed without changes.

‎doc/glossary/identities.hpp‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
#error This file is for documentation only - DO NOT INCLUDE
2+
/**
3+
4+
@page identity The Identity Elements (The "0" and "1" of Types)
5+
6+
@tableofcontents
7+
8+
* Just as there are neutral elements for the different mathematical operations, there are neutral elements for types.
9+
With this said, before building complex types, we must define the identities that govern type algebra.
10+
These types are the foundational "identity" elements.
11+
12+
---
13+
14+
@section empty Empty Type : \f$ (0 / \bot) \f$
15+
16+
The **Empty Type** is the identity element for **Sums** \f$ (A + 0 \cong A ) \f$.
17+
* **Cardinality**: 0 states. It is mathematically impossible to construct an instance of this type.
18+
* **Algebraic Role**: In logic, it represents a contradiction. In code, it represents a path that can never be taken.
19+
A function returning the Empty Type is a "diverging" function (it never returns).
20+
* **Identity Property**: Just as \f$ x + 0 = x \f$, having a choice between Type A or an impossible Type 0 is logically
21+
equivalent to simply having Type A.
22+
23+
One cannot write such a type, but could specify a function that returns empty, in C++ this can be expressed the
24+
following way.
25+
```cpp
26+
[[noreturn]] void foo(){ }
27+
```
28+
29+
---
30+
31+
@section unit Unit Type : \f$ (1 / \top) \f$
32+
33+
The **Unit Type** is the identity element for **Products** \f$ (A \times 1 \cong A) \f$.
34+
Also refered to as the product of no types.
35+
36+
* **Cardinality**: 1 state. It contains exactly one possible value (often written as `()`).
37+
* **Algebraic Role**: It represents "no information" or "success without data." Because there is only one possible state,
38+
the value itself is predictable and thus carries zero entropy.
39+
* **Identity Property**: Just as \f$ x \times 1 = x \f$, a pair containing Type A and a Unit Type provides no more
40+
information than Type A alone.
41+
42+
In C++ such a type can be written simply as a singleton.
43+
```cpp
44+
struct unit {};
45+
```
46+
47+
[In the next page](@ref product), we will see how to combine these simple types in order to compose what we call
48+
product types which is the main topic of kumi.
49+
50+
**/

‎doc/glossary/introduction.hpp‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
#error This file is for documentation only - DO NOT INCLUDE
2+
/**
3+
4+
@page introduction Type Theoretic Foundations
5+
6+
This introduction does not aim at providing full understanding of type theory, but is more focused on giving a brief yet
7+
extensive overview of the basis that might be of interest to any new or even experienced programmer. Kumi makes extensive
8+
use of some concepts that will be detailed in the following sections.
9+
10+
@section origin Origin
11+
12+
**Type Theory** is the academic study of type systems used to formalize how types are constructed and composed.
13+
While Set Theory categorizes elements into sets, Type Theory categorizes data (propositions) and the transformations
14+
(proofs) applied to them.
15+
16+
In this view:
17+
18+
* **Types** are classifications of data (propositions).
19+
* **Functions/Programs** are the logical steps that transform data (proofs).
20+
21+
---
22+
23+
@section curry_howard The Curry-Howard Correspondence
24+
25+
The **Curry-Howard Correspondence** formalizes the direct link between logical reasoning and type-level reasoning.
26+
Every concept in logic has a direct counter part in type theory.
27+
The following table recapitulates the different operation that can be necessary to understand.
28+
29+
| Logic Name | Logic Notation | Type Notation | Type Name | C++ Example |
30+
| :------------ | :-------------------| :-------------------| :----------------------| :-----------------------|
31+
| True | \f$ \top \f$ | \f$ \top \f$ | Unit Type | `std::monostate` |
32+
| False | \f$ \bot \f$ | \f$ \bot \f$ | Empty Type | `void` |
33+
| Implication | \f$ A \to B \f$ | \f$ A \to B \f$ | Function | `std::function<B(A)>` |
34+
| Not | \f$ \neg A \f$ | \f$ A \to 0 \f$ | Function to empty type | `[[noreturn]] void foo` |
35+
| And | \f$ A \land B \f$ | \f$ A \times B \f$ | Product type | `std::tuple<A,B>` |
36+
| Or | \f$ A \lor B \f$ | \f$ A + B \f$ | Sum type | `std::variant<A,B>` |
37+
38+
---
39+
40+
@section fundamentals Fundamentals
41+
42+
In order to be able to build more complex type, it is necessary to first define Atomic Terms. In common type theory,
43+
these can be of three different types. There are the natural numbers, often denotated *nat*, then there are boolean
44+
values notated *bool* and formal variables. Formal variables are simply variables reffered to by a symbol.
45+
46+
```cpp
47+
true : bool // A boolean
48+
42 : nat // A natural number
49+
x : bool // A formal variable
50+
```
51+
52+
Then in order to be able to manipulate these types, there is the concept of functions terms. This is simply a function
53+
in the programming sens. Given a parameter of a type \f$ \sigma \f$ and a return type \f$ \tau \f$ the associated function
54+
is noted \f$ \sigma \rightarrow \tau \f$. The addition of two real numbers can then written as :
55+
\f$ add : *nat* \rightarrow (*nat* \rightarrow *nat*)\f$
56+
57+
Finally, there are lambda terms, it is associated to concept of anonymous functions/lambdas functions in programming,
58+
these should sound familiar. They simply represent a way to define new function terms.
59+
60+
[In the next page](@ref identity), we will see some more specific types that are used as a base for more complex
61+
operations.
62+
63+
---
64+
65+
* **Reference** [Wikipedia: Type Theory](https://en.wikipedia.org/wiki/Type_theory)
66+
67+
**/

doc/nomenclature.md renamed to doc/glossary/nomenclature.md

File renamed without changes.

‎doc/glossary/product.hpp‎

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
#error This file is for documentation only - DO NOT INCLUDE
2+
/**
3+
4+
@page product Product Types
5+
6+
@tableofcontents
7+
8+
@section product_construction Product Constructions (The Logic of "AND")
9+
10+
Products represent types where multiple elements exist simultaneously.
11+
The operands of the product are types.
12+
The structure of a product type is determined by the fixed order of the operands.
13+
14+
@subsection product_type Product Type \f$ (A \times B) \f$
15+
16+
A **Product Type** is a compound type formed by combining multiple types.
17+
18+
An instance of a product type in it's simplest form is a called a tuple.
19+
20+
Such a type only accepts one constructor that takes a variadic number of inputs
21+
and builds the product of them. A product type has a fixed length and the types of
22+
the elements is fixed. Formally it can be written as :
23+
24+
\f$ (x_1, x_2, ..., x_n) : T_1 \times T_2 \times ... \times T_n \f$
25+
26+
This can be read as : the tuple is composed of elements of types \f$ T_1 \f$ to \f$ T_n\f$
27+
with corresponding values \f$ x_1 \f$ to \f$ x_n \f$.
28+
29+
The corresponding definition in kumi could look like the following:
30+
```cpp
31+
kumi::tuple<int,float,char> a = { 42, 13.37f, 'd' };
32+
```
33+
34+
To extract values from a tuple, there are projections that are term constructors.
35+
A projection (often noted \f$ \pi \f$) is a function that given a product type
36+
returns the elements. Formally it is denoted as :
37+
38+
\f$ \pi_1(x) : T_1, \pi_2(x) : T_2, ..., \pi_n(x) : T_n \f$
39+
40+
In kumi this corresponds to the `get` functions
41+
```c
42+
auto a = kumi::get<0>(kumi::tuple<int,float>{ 1, 2.f });
43+
```
44+
45+
A product type follows **List Algebra**.
46+
+ **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.
47+
+ **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$.
48+
49+
### Example
50+
```cpp
51+
std::tuple<int, float> p; // Ordered product
52+
```
53+
54+
@note A pair is a special case of a tuple that is composed of only two elements.
55+
56+
* **Reference** [Wikipedia: Tuple](https://en.wikipedia.org/wiki/Tuple)
57+
58+
---
59+
60+
@subsection record_type Record Type \f$ \{label: Type\} \f$ (The Struct)
61+
62+
A **Record Type** identifies its components by a **unique label** rather than a position.
63+
64+
An instance of a record type is called a struct in many programming languages.
65+
(Let aside considerations about object oriented progamming, inheritance, etc...)
66+
67+
A **Record Type** is the labeled version of a Product, it can be seen as the product of mathematical sets.
68+
It follows **Set Algebra** on top of **List Algebra**.
69+
70+
Operation on records are traditionally not structural in the sens that they operate per label, never per
71+
element. However, as they are internally represented by a tuple, such operation are permitted. As an example, one
72+
could "rotate" a record \f$ n \f$ positions to the left. Mathematically this might not make a lot of sens
73+
whereas for a programmer that has to consider memory representation, this is potentially critical to have.
74+
75+
+ **Label Identity**: Components are identified by unique **Labels** (names) rather than position.
76+
+ **Permutation**: Theoretically, a record is a set of field mappings. In many formal definitions, `{x: int, y: float}`
77+
is isomorphic to `{y: float, x: int}` because the set of labels and their associated types are identical.
78+
+ **Semantic Access**: Access is performed via labels (`u.id`), adding semantic meaning to the structure.
79+
80+
### Example
81+
```cpp
82+
struct User {
83+
int id; // Label: id
84+
float score; // Label: score
85+
};
86+
```
87+
88+
* **Reference** [Wikipedia: Record](https://en.wikipedia.org/wiki/Record_(computer_science))
89+
90+
[In the next page](@ref sum), we will see the duals of product types which are called sum types.
91+
92+
**/

‎doc/glossary/sum.hpp‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
#error This file is for documentation only - DO NOT INCLUDE
2+
/**
3+
4+
@page sum Sum Types
5+
6+
@tableofcontents
7+
8+
@section sum_construction Sum Constructions (The Logic of "OR")
9+
10+
Sums represent types where a choice is made between different alternatives. They are the mathematical **Dual** of Products.
11+
12+
@subsection sum_type Sum Type \f$ (A + B) \f$ (The Coproduct)
13+
14+
An unlabeled, positional choice between types.
15+
* **Exclusive Choice**: An instance of \f$ A + B \f$ contains either an A or a B, but never both simultaneously.
16+
* **Cardinality**: The state space is the **sum** of its components: \f$ Card(A + B) = Card(A) + Card(B) \f$.
17+
* **Algebraic Property**: It is the dual of the Product. While a Product asks you to "Take All," a Sum asks you to "Pick One."
18+
19+
### Example
20+
```cpp
21+
std::variant<int, float> p;
22+
```
23+
24+
@subsection variant Variant (The Labeled Sum)
25+
A **Variant** is the labeled version of a Sum Type (and thus the dual of the Record).
26+
* **Active Labeling**: Just as a Record has multiple labels present at once, a Variant has exactly **one active label** from a set of possibilities.
27+
* **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.
28+
29+
### Example
30+
```cpp
31+
union particles {
32+
muons m;
33+
leptons l;
34+
quarks q;
35+
};
36+
```
37+
38+
**/

‎doc/glossary/type_theory.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
Type-Theoretic Foundations {#type_theory}
2+
----------
3+
4+
## Introduction
5+
6+
---
7+
8+
## Monoid
9+
A type is a **Monoid** if it possesses a binary operation to combine elements and an identity element.
10+
It needs to model other mathematical laws such as :
11+
1. **Associativity:** \f$ (a + b) + c = a + (b + c) \f$.
12+
2. **Identity Element:** \f$ a + Identity = a \f$.
13+
14+
**Example:** `std::string` is a monoid where the operation is `+` (concatenation) and the identity is `""`.

‎doc/layout.xml‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,12 @@
99
<tab type="user" url="@ref licence" title="Licence"/>
1010
</tab>
1111
<tab type="usergroup" visible="yes" title="Glossary">
12-
<tab type="user" url="@ref type_theory" title="Type Theory"/>
12+
<tab type="usergroup" visible="yes" title="Type Theory">
13+
<tab type="user" url="@ref introduction" title="Introduction"/>
14+
<tab type="user" url="@ref identity" title="Identity Types"/>
15+
<tab type="user" url="@ref product" title="Product Types"/>
16+
<tab type="user" url="@ref sum" title="Sum Types"/>
17+
</tab>
1318
<tab type="user" url="@ref cpp_spec" title="C++ Vocabulary"/>
1419
<tab type="user" url="@ref nomenclature" title="Nomenclature"/>
1520
</tab>

0 commit comments

Comments
 (0)