feat(report): add section about types

report/chapters/03_theory.typ

@@ -128,7 +128,7 @@ A particularity of Midas are its constraint types. A constraint type `T where e`
 
 Now that we have defined what Python syntax we will support and our own definition language, we need to define how our type checker will be able to bind types to Python expressions. This section is heavily inspired by the _Pure simply typed lambda-calculus~($lambda_->$)_, _Simply typed lambda-calculus with subtyping~($lambda_(<:)$)_, _Polymorphic lambda-calculus (System F)_ and _Bounded quantification (kernel $F_(<:)$)_ presented in Chapters 9, 15, 23 and 26 of #acr("TaPL")@tapl.
 
-=== Literals
+=== Literals <sec:typing-literals>
 
 First and foremost, we can define elementary typing rules for all literal values. These rules having no premises, they are simple axioms. @tab:typing-literals lists all literal typing rules.
 
@@ -141,7 +141,7 @@ First and foremost, we can define elementary typing rules for all literal values
 
 Other constructs, although not constants, directly map to builtin types. These include literal lists, tuples and dictionaries. Each of these has a corresponding `list[T]`, `tuple` and `dict[K, V]` type. We will not define formal rules in this section regarding these elements, but a more in depth explanation will be given in the implementation of the type checker, in @sec:impl-python. #todo[replace ref]
 
-=== Expressions
+=== Expressions <sec:typing-expressions>
 
 Apart from literals, developers also need some building blocks to express their programs. These expressions include variables, function calls, operations, etc. and need their own typing rules. The rules listed in @tab:typing-expressions cover most expressions we will handle, as defined in @sec:theory-syntax-python. Some syntaxes are omitted to keep this chapter short and because they don't necessarily bring new theoretical concepts.
 
@@ -160,7 +160,7 @@ Apart from literals, developers also need some building blocks to express their
 
 #smallcaps[T-Op] is used for all binary operations. In Python, these are implemented in _dunder-methods_, such as `__add__` for the `+` operator. A similar rule could be defined for unary operations but is omitted here for brevity.
 
-=== Statements
+=== Statements <sec:typing-statements>
 
 Finally, expressions can be used in statements, which are special constructs that can have side-effects. We listed in @sec:theory-syntax-python the particular statements that Midas should support, and @tab:typing-statements provides rules to type check their components and effects.
 
@@ -183,7 +183,7 @@ Finally, expressions can be used in statements, which are special constructs tha
 
 #smallcaps[T-Def] is a gross simplification of how functions can be defined. It does not cover multiple parameters, positional-only and keyword-only parameters, complex bodies with multiple and implicit returns, etc. Again, for the sake of simplicity and readability, we will not define a complete rule to handle all forms and features, but the implementation will go into more details in @sec:impl-python. #todo[replace ref]
 
-=== Subtyping
+=== Subtyping <sec:typing-subtyping>
 
 Similarly to some calculi described in #acr("TaPL")@tapl and to allow flexibility, we must equip our type system with a subtyping relationship. This relationship allows using some types in place of others where it is sound to do so. The subtyping rules presented in @tab:typing-subtyping-base cover the base cases of subtyping.
 
@@ -219,7 +219,7 @@ Finally, functions in Python are complex types. The general subtyping rule is gi
   supplement: [Table],
 ) <tab:typing-subtyping-function>
 
-=== Special types
+=== Special types <sec:theory-special-types>
 
 Two special types can be added to our type system for practical purposes. The first is a regular top type, as represented by `Any` in Python. Every type is a subtype of `Any`, as stated by #smallcaps[S-Any] in @tab:typing-subtyping-top.
 

report/chapters/04_implementation.typ

@@ -21,9 +21,10 @@ In @sec:impl-overview, we will first look at the whole system from a top-down pe
 #pagebreak()
 
 #include-offset(path("04_implementation/01_overview.typ"))
-#include-offset(path("04_implementation/02_midas_language.typ"))
-#include-offset(path("04_implementation/03_python_checking.typ"))
-#include-offset(path("04_implementation/04_generation.typ"))
+#include-offset(path("04_implementation/02_types_registry.typ"))
+#include-offset(path("04_implementation/03_midas_language.typ"))
+#include-offset(path("04_implementation/04_python_checking.typ"))
+#include-offset(path("04_implementation/05_generation.typ"))
 
 /*
 Subjects:

report/chapters/04_implementation/02_types_registry.typ

@@ -0,0 +1,151 @@
+#import "../../requirements.typ": isc-hei-bthesis
+#import isc-hei-bthesis: todo
+#import "../../utils.typ": fn-link, code-ref
+#import "@preview/acrostiche:0.7.0": acr
+
+= Internal Type Representations <sec:impl-types>
+
+Before we can parse type definitions or type check Python code, we need to define structures to represent our types.
+
+In our type system, we will indeed have different kind of types with different properties.
+
+== Base Types
+
+The simplest types are those at the root of the type lattice with no or few properties. These include top-types like `Any`, `UnknownType` and `UnitType`/`None`, as described in @sec:theory-special-types, which can be represented as simple empty classes like in @fig:types-base-types. Builtin types also have a dedicated `BaseType` kind which holds the type's name.
+For the special `tuple` type, we can define a more specific class which can hold the each item's type. This will allow nice type checking of subscript expressions for example.
+
+#figure(
+  ```python
+  class TopType: ...
+  class UnknownType: ...
+  class UnitType: ...
+  class BaseType:
+      name: str
+  class TupleType:
+      items: tuple[Type, ...]
+  ```,
+  caption: [Type kinds: base types]
+) <fig:types-base-types>
+
+== Derived Types
+
+When defining subtypes in Midas, we will need to store that link in the registry. There are multiple approaches to subtyping, which can either be nominal or structural. In the case of Midas, we will generally stick to nominal subtyping, i.e. subtypes are explicitly defined, with some exceptions like constraint types and function types, as described in @sec:typing-subtyping.
+
+Instead of storing the subtype relationship in a separate registry, we will embed it in the type itself by using a `DerivedType` class containing the type's name and super-type. This allows easy pattern matching without additional queries to the registry, and keeps the type hierarchy clear and explicit.
+A similar approach is used for constraint types, by embedding the base type and the constraint expression in the same `ConstraintType` object, as shown in @fig:types-derived-types.
+
+#figure(
+  ```python
+  class DerivedType:
+      name: str
+      type: Type
+  class ConstraintType:
+      type: Type
+      constraint: m.Expr
+  ```,
+  caption: [Type kinds: derived types]
+) <fig:types-derived-types>
+
+== Generic Types
+
+To define generic types, we first need type variables, which are kinds of placeholder types. These type variables have a name, an optional bounding type and a variance. The latter can be represented as a simple enum. As explained in @sec:typing-subtyping, variance is inferred rather than explicitly annotated by the user. This inference process is described in @sec:impl-midas #todo[replace ref].
+Once type variables are defined, generic types are simply a kind of derived type with a list of parameters.
+We also need to define an application counterpart to represent a generic type that has been instantiated with some concrete type arguments. Here, the choice of having this `AppliedType` kind instead of simply using the generic's body with its parameters substituted has been made for multiple reasons. Most importantly, it allows diagnostics to be more specific and informative and eases some comparisons between different applied types.
+
+These types are implemented by the classes in @fig:types-generics.
+
+#figure(
+  ```python
+  class Variance(StrEnum):
+      INVARIANT = "INVARIANT"
+      COVARIANT = "COVARIANT"
+      CONTRAVARIANT = "CONTRAVARIANT"
+  class TypeVar:
+      name: str
+      bound: Optional[Type]
+      variance: Variance = Variance.INVARIANT
+  class GenericType:
+      name: str
+      params: list[TypeVar]
+      body: Type
+  class AppliedType:
+      name: str
+      args: list[Type]
+      body: Type
+  ```,
+  caption: [Type kinds: generic types]
+) <fig:types-generics>
+
+== Function Types
+
+As noted in the theory chapter (@chap:theory), functions in Python are complex and highly flexible.
+A function type thus have a parameter specification and a return type. That parameter specification contains three kinds of parameters: positional-only (`pos`), keyword-only (`kw`) and mixed (`mixed`).
+@fig:types-functions shows the implemented structures to handle function types and their parameters.
+For simplicity, each parameter will store both its position and name, as well as its type and a flag indicating whether it is required or not (e.g. parameters with default values are optional). You may notice an additional `unsupported` flag in @fig:types-functions:10, which is added for some dataframe-related methods. More information shall be given in @sec:impl-python #todo[replace ref].
+
+Finally, we will also define a structure to hold multiple signature of an overloaded function because it cannot be represented as a single `Function`. You may also notice that `OverloadedFunction.overloads` does not store a list of `Function` but simply a list of `Type`, in @fig:types-functions:16. This allows the use of generic functions, which are `Function` types wrapped inside a `GenericType`.
+
+#figure(
+  ```python
+  class Function:
+      params: ParamSpec
+      returns: Type
+
+      class Parameter:
+          pos: int
+          name: str
+          type: Type
+          required: bool
+          unsupported: bool = False
+  class ParamSpec:
+      pos: list[Function.Parameter] = field(default_factory=list)
+      mixed: list[Function.Parameter] = field(default_factory=list)
+      kw: list[Function.Parameter] = field(default_factory=list)
+  class OverloadedFunction:
+      overloads: list[Type]
+  ```,
+  caption: [Type kinds: function types]
+) <fig:types-functions>
+
+== Dataframe types
+
+Because Midas has been designed with data scientists in mind, it will also try and type check some common dataframe operations. To do so, we want the user to be able to define dataframe schemas and use their columns. We thus define `ColumnType` and `DataFrameType` in @fig:types-dataframes, which can be thought of as more abstract representations of Pandas' `Series` and `DataFrame`. Additionally, we define special objects to handle group-by entities which are intermediary values used when computing aggregations. These group-by types are necessary to distinguish them from the base dataframe or column because they provide different methods.
+
+#figure(
+  ```python
+  class ColumnType:
+      type: Type
+  class DataFrameType:
+      columns: list[Column]
+
+      class Column:
+          index: int
+          name: Optional[str]
+          type: ColumnType
+  class FrameGroupBy:
+      frame: DataFrameType
+  class ColumnGroupBy:
+      column: ColumnType
+  ```,
+  caption: [Type kinds: dataframe types]
+) <fig:types-dataframes>
+
+== Predicates
+
+Although not types, predicates will also be represented by similar dataclasses in the types registry, as defined in @fig:types-predicate.
+
+#figure(
+  ```python
+  class Predicate:
+    type: Type
+    body: m.Expr
+    alias: bool
+  ```,
+  caption: [Predicate Dataclass]
+) <fig:types-predicate>
+
+This class holds three properties of predicates:
+- `type`: the function signature of the predicate.\
+  For example, ```midas predicate less_than(max: float)(v: float) = v < max``` has the signature ```midas fn(max: float) -> fn(v: float) -> bool```
+- `body`: the raw predicate expression. This will be used to generate equivalent Python code and perform static checks against literal values
+- `alias`: a flag indicating whether a predicate is a simple alias of another, used for example with partially applied predicates (see @sec:impl-midas #todo[replace ref])

report/chapters/04_implementation/03_midas_language.typ

@@ -75,6 +75,66 @@ The complete implementations of `MidasLexer` and `MidasParser` are available in
 - `MidasParser`: #code-ref(<midas-parser>, "midas/parser/midas.py")
 - `Parser` (base class): #code-ref(<parser>, "midas/parser/base.py")
 
+Let's take a simple example of some Midas source code to highlight the different steps of the process:
+
+#figure(
+  ```midas
+  type Kelvin = float where _ >= 0
+  ```,
+  caption: [Midas Example: source code]
+) <fig:example-midas-src>
+
+@fig:example-midas-src is first passed through the lexer which outputs a sequence of tokens, as shown in @fig:example-midas-tokens.
+
+#figure(
+  ```python
+  [
+    Token(type=TokenType.TYPE,         lexeme='type',  value=None,position="L1:1"),
+    Token(type=TokenType.WHITESPACE,   lexeme=' ',     value=None,position="L1:5"),
+    Token(type=TokenType.IDENTIFIER,   lexeme='Kelvin',value=None,position="L1:6"),
+    Token(type=TokenType.WHITESPACE,   lexeme=' ',     value=None,position="L1:12"),
+    Token(type=TokenType.EQUAL,        lexeme='=',     value=None,position="L1:13"),
+    Token(type=TokenType.WHITESPACE,   lexeme=' ',     value=None,position="L1:14"),
+    Token(type=TokenType.IDENTIFIER,   lexeme='float', value=None,position="L1:15"),
+    Token(type=TokenType.WHITESPACE,   lexeme=' ',     value=None,position="L1:20"),
+    Token(type=TokenType.WHERE,        lexeme='where', value=None,position="L1:21"),
+    Token(type=TokenType.WHITESPACE,   lexeme=' ',     value=None,position="L1:26"),
+    Token(type=TokenType.UNDERSCORE,   lexeme='_',     value=None,position="L1:27"),
+    Token(type=TokenType.WHITESPACE,   lexeme=' ',     value=None,position="L1:28"),
+    Token(type=TokenType.GREATER_EQUAL,lexeme='>=',    value=None,position="L1:29"),
+    Token(type=TokenType.WHITESPACE,   lexeme=' ',     value=None,position="L1:31"),
+    Token(type=TokenType.NUMBER,       lexeme='0',     value=0,   position="L1:32"),
+    Token(type=TokenType.EOF,          lexeme='',      value=None,position="L1:33")
+  ]
+  ```,
+  caption: [Midas Example: tokens]
+) <fig:example-midas-tokens>
+
+These tokens are then passed through the parser which builds an #acr("AST") shown in @fig:example-midas-ast. This representation is produced by the `MidasASTPrinter` class which can be used via a dedicated command: ```sh midas parse file.midas```. More information about available commands are given in the dedicated #fn-link(<manual>, "https://git.kb28.ch/HEL/midas/src/branch/main/docs/manual.pdf")[manual].
+
+#figure(
+  ```AST
+  TypeStmt
+  ├── name: "Kelvin"
+  ├── params
+  └── type
+      └── ConstraintType
+          ├── type
+          │   └── NamedType
+          │       └── name: "float"
+          └── constraint
+              └── BinaryExpr
+                  ├── left
+                  │   └── WildcardExpr
+                  ├── operator: >=
+                  └── right
+                      └── LiteralExpr
+                          └── value: 0
+  ```,
+  caption: [Midas Example: #acr("AST")]
+) <fig:example-midas-ast>
+
+After passing through `MidasParser`, we thus obtain a stable and explicit structure that can be given to `MidasTyper` and interpreted (as far as a definition language can be interpreted).
 
 == Processing statements