fix(report): chapter heading supplement

report/appendices/function_subtyping.typ

@@ -17,7 +17,7 @@ $ p = (i, n, r) $
 A *Function* has a param spec $S$ and a return type $R$:
 $ F = (S, R) $
 
-= Main rules
+= Main Rules
 
 We want to define a rule for checking structural subtyping of functions, i.e. to check when $F_1 <: F_2$
 
@@ -39,7 +39,7 @@ After mapping parameters of $S_1$ and $S_2$, types must be checked such that if
 
 #pagebreak(weak: true)
 
-= Detailed rules for *ParamSpec* subtyping
+= Detailed Rules for *ParamSpec* Subtyping
 
 #gc.info(title: [Notation])[
   In the following equations:
@@ -51,7 +51,7 @@ After mapping parameters of $S_1$ and $S_2$, types must be checked such that if
   - $req(S, alpha)$ is a predicate checking whether $alpha$ is required in $S$
 ]
 
-== Arguments of $S_2$ are compatible with $S_1$ <cond-1>
+== Arguments of $S_2$ are Compatible with $S_1$ <cond-1>
 
 Formally, the condition is:
 $
@@ -77,7 +77,7 @@ $
   )
 $
 
-== No additional required arguments in $S_1$ <cond-2>
+== No Additional Required Arguments in $S_1$ <cond-2>
 
 Formally, the condition is:
 $

report/bachelor_thesis.typ

@@ -148,6 +148,10 @@ This structure may vary depending on the field of study, but these elements are
 You can also change the order or the names of the sections, for instance, if you want to put the state of the art before the introduction, or if you want to add a section on methodology before the results.
 */
 
+#show heading.where(level: 1): set heading(supplement: context {
+  let f = inc.global-language.get()
+  i18n(f, "chapter-title")
+})
 #include "chapters/01_introduction.typ"
 #include "chapters/02_state_of_the_art.typ"
 #include "chapters/03_theory.typ"
@@ -191,11 +195,14 @@ You can also change the order or the names of the sections, for instance, if you
 
 #counter(heading).update(0)
 
-#set heading(numbering: "A.1", supplement: [Appendix])
+#set heading(numbering: "A.1")
 
 #set figure(numbering: (..nums) => counter(heading).display("A.1") + "." + numbering("1", ..nums))
 #set heading(outlined: false)
-#show heading.where(level: 1): set heading(outlined: true)
+#show heading.where(level: 1): set heading(
+  outlined: true,
+  supplement: [Appendix]
+)
 #counter(figure.where(kind: image)).update(0)
 #counter(figure.where(kind: table)).update(0)
 #counter(figure.where(kind: raw)).update(0)

report/chapters/01_introduction.typ

@@ -8,7 +8,7 @@
   Any one who considers arithmetical methods of producing random digits is, of course, in a state of sin
 ]
 
-Dogs are often said to be man's best friend for their unwavering loyalty. As human beings, we thrive on patterns and predictability. On the other hand, our little animal friends can sometimes be irrational and surprise us with their unpredictable behavior. Computers however, these thought-less automatic machines made of metal, would be much better companions.
+Dogs are often said to be man's best friends for their unwavering loyalty. As human beings, we thrive on patterns and predictability. On the other hand, our little animal friends can sometimes be irrational and surprise us with their unpredictable behavior. Computers however, these thought-less automatic machines made of metal, would be much better companions.
 
 By their fundamental essence, computers and other similar machines are deterministic. As developers, we simply give them series of instructions, algorithms, functions and other scripts. Their one and only job is to execute our commands, one after the other, sometimes at the same time. An addition is always an addition, a byte is always a byte, and most importantly, a dog is always a dog.
 
@@ -25,11 +25,11 @@ Additionally, the Python language uses dynamic typing, a design principle allowi
 
 == Motivation
 
-As explained above, Python is a very flexible language, sometimes too flexible. For beginners trying to learn programming, this can be a double-edged sword. One the one hand, the language is quite lenient and allows mixing data types, reusing variables with different types and passing values that are not at all what was expected by a function but still have the correct attributes or methods. On the other hand, it can lead to confusing behavior, when a parameter does not fit the developer's expectation or a variable is changed in some part of the code to a completely different kind of value. At the professional level, this can also prove dangerous. Mixing medical measurements or having a production service crash because of a type error can become an expensive mistake with real-world impact.
+As explained above, Python is a very flexible language, sometimes too flexible. For beginners trying to learn programming, this can be a double-edged sword. On the one hand, the language is quite lenient and allows mixing data types, reusing variables with different types and passing values that are not at all what was expected by a function but still have the correct attributes or methods. On the other hand, it can lead to confusing behavior, when a parameter does not fit the developer's expectations or a variable is changed in some part of the code to a completely different kind of value. At the professional level, this can also prove dangerous. Mixing medical measurements or having a production service crash because of a type error can become an expensive mistake with real-world impact.
 
 Secondly, as every Java developer can tell you, runtime errors are the worst. The dreaded `NullPointerException` continues to haunt many developers. Although some runtime errors like this are quite loud and can crash an hour-long computation process, others are much more subtle and tricky to catch. A famous example of this is the historical crash of NASA's Mars Climate Orbiter in 1999, which failed its orbital insertion due to a unit error mixing metric and imperial measurements.@MCOReport
 
-Lastly, designing a safe code base and including tests to check that values conform to what is expected can be a tedious and often unrewarding process. Simplifying this process is one of the motivation for the famous Python library Pydantic, allowing users to define data structures that can validate inputs when instantiated.
+Lastly, designing a safe code base and including tests to check that values conform to what is expected can be a tedious and often unrewarding process. Simplifying this process is one of the motivations for the famous Python library Pydantic, allowing users to define data structures that can validate inputs when instantiated.
 
 == Objectives
 

report/chapters/02_state_of_the_art.typ

@@ -7,13 +7,13 @@
 
 First of all, before reinventing the wheel and creating a completely redundant tool, we must look at what already exists in Python's rich environment and beyond.
 
-The Python Language includes a dedicated syntax for what are called "type hints", as defined in PEP 484 since Python 3.5@PEP484.
-Type hints are annotations that users can add to variables and functions to specify information about the type of some values.
+The Python language includes a dedicated syntax for what are called "type hints", as defined in PEP 484 since Python 3.5@PEP484.
+Type hints are annotations that users can add to variables and functions to specify information about the types of some values.
 
 Python also natively provides a `typing` module with several tools developers can use to better describe their code. This includes but is not limited to `Generic` and `TypeVar` for generic types, the `cast()` function, the `TypeAlias` class to explicitly mark some assignments as type aliases, and `Protocol`, a multipurpose machinery allowing the definition of interface-like classes (defined since Python 3.8 in PEP 544@PEP544). The latter can notably be used to remove some ambiguity around duck-typing and make it more explicit, by indicating that some value implements some method or has some specific attribute.\
-However, this system is difficult to scale to dataframe and more complex type operations. Additionally, Python remains a fundamentally dynamically typed language which only really cares about the values' base types and whether they possess specific attributes or methods.
+However, this system is difficult to scale to dataframes and more complex type operations. Additionally, Python remains a fundamentally dynamically typed language which only really cares about the values' base types and whether they possess specific attributes or methods.
 
-Of course, type checkers have long been integrated into IDEs, like MyPy and Pyright. These often provide comprehensive type checking, supporting all aforementioned features of the `typing` module and more, and often offer multiple levels of strictness. They do lack some features that could give users more freedom in defining type aliases such as a generic type that is a subtype of its own parameter (e.g. a `Price[EUR]` is an amount of `EUR`, which is itself a `float`). They do not support constraint type either and only provide static analysis, without the ability to generate runtime assertions. Type checking complex structures like `numpy` arrays or `pandas` dataframes is also complicated, if not impossible.
+Of course, type checkers have long been integrated into IDEs, like MyPy and Pyright. These often provide comprehensive type checking, supporting all aforementioned features of the `typing` module and more, and often offer multiple levels of strictness. They do lack some features that could give users more freedom in defining type aliases such as a generic type that is a subtype of its own parameter (e.g. a `Price[EUR]` is an amount of `EUR`, which is itself a `float`). They do not support constraint types either and only provide static analysis, without the ability to generate runtime assertions. Type checking complex structures like `numpy` arrays or `pandas` dataframes is also complicated, if not impossible.
 
 In Python's ecosystem, there are two interesting projects which do however try to help with typing dataframes. The first, focused on statically typing schemas, is called #fn-link(<strictly-typed-pandas>, "https://strictly-typed-pandas.readthedocs.io")[_Strictly Typed Pandas_]. It allows declaring schemas as simple class definitions and even provides runtime verification using a simple `@typechecked` decorator. In spite of that, it does seem to lack proper type checking of operations on dataframes and columns.
 The other project worth mentioning is called #fn-link(<pandera>, "https://pandera.readthedocs.io")[_Pandera_]@niels_bantilan-proc-scipy-2020. This Python package provides a wide range of features to perform runtime verification of dataframe schemas and data validation, such as statistical analysis. While it does seem to be a rather useful and complete tool, it does not cover our static type checking goal and has quite a verbose syntax.

report/chapters/03_theory.typ

@@ -81,11 +81,11 @@ Finally, the rules expressed in @sec:theory-syntax are written in the form of th
 
 #pagebreak(weak: true)
 
-== Syntax rules <sec:theory-syntax>
+== Syntax Rules <sec:theory-syntax>
 
 In this section, we define syntax rules for both Python and our type definition language Midas. Obviously, Python already has syntax rules defining what is or is not valid code. What is defined in @sec:theory-syntax-python are a subset of constructs which our type checker will be able to process.
 
-=== Python syntax <sec:theory-syntax-python>
+=== Python Syntax <sec:theory-syntax-python>
 
 @tab:python-syntax-rules lists mosts Python constructs we want to support with our type checker (notable exceptions are listed below). This subset of the Python language is sufficient to express a wide range of programs, including data processing pipelines and moderately complex scripts.
 
@@ -98,9 +98,9 @@ In this section, we define syntax rules for both Python and our type definition
 
 Some syntaxes are simplified or omitted from @tab:python-syntax-rules for the sake of conciseness, readability and scope. Indeed, this work's primary focus is not on the theoretical and formal approach to type checking but rather on the concrete application of it to produce a useful tool for developers. For example, function signature in Python are rather complex and flexible, allowing positional-only, keyword-only and mixed parameters, argument sinks, and default values. Expressing this level of flexibility in a formal definition as those presented above is tricky and not necessarily pertinent to this work.
 
-Other syntaxes not referenced in this report are voluntarily left out because they either fall out of the scope of this work or are either not fundamental to the language or not necessary to most developers. Such constructs include classes, match statements, while loops, `for`/`else` blocks and the walrus operator~(`:=`).
+Other syntaxes not referenced in this report are voluntarily left out because they either fall out of the scope of this work, are not fundamental to the language or not necessary to most developers. Such constructs include classes, match statements, while loops, `for`/`else` blocks and the walrus operator~(`:=`).
 
-=== Midas syntax <sec:theory-syntax-midas>
+=== Midas Syntax <sec:theory-syntax-midas>
 
 Our type system includes a dedicated language to define custom types that can be used in Python code. This language is hereafter referred to as the Midas language, or simply Midas. Its goal is to allow users to concisely define types, aliases, subtypes and the like in a simple and intuitive language. All syntax rules are listed in @tab:midas-syntax-rules.
 
@@ -120,13 +120,13 @@ A more detailed definition of the syntax is available in @app:midas-syntax.
 
 Some elements are worth explaining here. Midas offers four base statements through four keywords: `alias`, `type`, `extend` and `predicate`.\
 The first is rather straightforward: ```midas alias X = T``` defines an alias named `X` for the type `T`.\
-The second is a simple subtype definition. ```midas type X = T``` is similar to an alias, but it creates a subtype relationship instead of an equivalence. `X` is thus a subtype of `T`. This also allows defining generic types using type parameters, bounded or not, which can be referenced in the right-hand side of the definition. For example ```midas type Foo[T <: U] = list[T]``` defines a type generic `Foo` with one parameter `T` subtype of `U`, which is a subtype of `list[T]`.\
+The second is a simple subtype definition. ```midas type X = T``` is similar to an alias, but it creates a subtype relationship instead of an equivalence. `X` is thus a subtype of `T`. This also allows defining generic types using type parameters, bounded or not, which can be referenced in the right-hand side of the definition. For example ```midas type Foo[T <: U] = list[T]``` defines a generic type `Foo` with one parameter `T` subtype of `U`, which is a subtype of `list[T]`.\
 The third, `extend`, is linked to a subtype definition. It allows users to define members on a type, such as properties/attributes (`prop`) and methods (`def`). Methods may be overloaded to combine multiple signatures under the same name. The type specified after `extend` must obviously be defined.\
-The last kind of statement provides user with a way to define named constraint expressions and reuse them as functions in other constraint expressions. Predicates are defined like functions, with a list of parameters. This list may be split into multiple parameter specifications, for example ```midas predicate foo(a: float)(b: int) = a < b``` to allow partial application.
+The last kind of statement provides users with a way to define named constraint expressions and reuse them as functions in other constraint expressions. Predicates are defined like functions, with a list of parameters. This list may be split into multiple parameter specifications, for example ```midas predicate foo(a: float)(b: int) = a < b``` to allow partial application.
 
 A particularity of Midas are its constraint types. A constraint type `T where e` is built from a base type `T` and a constraint expression `e`. It allows binding a constraint on the values belonging to this type, which will be materialized by assertions at runtime.
 
-== Typing rules <sec:theory-typing>
+== Typing Rules <sec:theory-typing>
 
 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.
 
@@ -204,12 +204,11 @@ Similarly to some calculi described in #acr("TaPL")@tapl and to allow flexibilit
   supplement: [Table],
 ) <tab:typing-subtyping-base>
 
-The subtyping relationship is by definition both reflective (#smallcaps[S-Refl]) and transitive (#smallcaps[S-Trans]).
-
+The subtyping relationship is by definition both reflective (#smallcaps[S-Refl]) and transitive (#smallcaps[S-Trans]).\
 #smallcaps[T-Sub] is a consequence of the #acr("LSP"). A term $"t"$ of type $"S"$ can be used anywhere a term of type $"T"$ is expected if $"S"$ is a subtype of $"T"$.
 
 In addition to these base rules, we need to define how functions, constraint types and generic types are handled.
-For constraint types, we will take the simple approach of considering only the base type for the subtype relationship. A more complete and interesting implementation could implement subtyping of constraint expression, where a condition such as `_ < 10` is a subtype of `_ < 100`, but the added complexity was deemed out of scope for this particular project. We do nonetheless define #smallcaps[S-Constr] in @tab:typing-subtyping-constraint to handle the base case.
+For constraint types, we will take the simple approach of considering only the base type for the subtype relationship. A more complete and interesting implementation could consider subtyping of constraint expression, where a condition such as `_ < 10` is a subtype of `_ < 100`, but the added complexity was deemed out of scope for this particular project. We do nonetheless define #smallcaps[S-Constr] in @tab:typing-subtyping-constraint to handle the base case.
 
 #figure(
   typing.subtyping-constraint,
@@ -218,7 +217,7 @@ For constraint types, we will take the simple approach of considering only the b
   supplement: [Table],
 ) <tab:typing-subtyping-constraint>
 
-Generics are handled using similar rules to the _Bounded quantification (kernel $F_(<:)$)_ calculus presented in #acr("TaPL") Chapter 26@tapl. Additionally, Midas supports implicit variance, which is inferred from the locations in which type parameters are used, and is used when checking subtypes of applied generic types. A detailed explanation of variance inference is provided in the corresponding implementation section, @sec:variance-inference.
+Generics are handled using similar rules to the _Bounded quantification (kernel $F_(<:)$)_ calculus presented in #acr("TaPL") Chapter 26@tapl. Additionally, Midas supports implicit variance, which is inferred from the locations in which type parameters are referenced, and is used when checking subtypes of applied generic types. A detailed explanation of variance inference is provided in the corresponding implementation section, @sec:variance-inference.
 
 Finally, functions in Python are complex types. The general subtyping rule is given in @tab:typing-subtyping-function, but the complete set of rules for checking parameter specifications is too complex to include here. It is however detailed in @app:function-subtyping.
 
@@ -229,7 +228,7 @@ Finally, functions in Python are complex types. The general subtyping rule is gi
   supplement: [Table],
 ) <tab:typing-subtyping-function>
 
-=== Special types <sec:theory-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/03_theory/midas_syntax.typ

@@ -10,10 +10,10 @@
 #let statements = (
   ($#syntax[alias] "X" = "T"$, [_alias definition_]),
   ($#syntax[type] "X" = "T"$, [_type definition_]),
-  ($#syntax[type] "X"["P"^(i in 1..n)] = "T"$, [_generic definition_]),
+  ($#syntax[type] "X"["P"_i^(i in 1..n)] = "T"$, [_generic definition_]),
   ($ cases(
-    #syntax[extend] "X"["P"^(i in 1..n)] space \{,
-    quad m^(j in 1..M),
+    #syntax[extend] "X"["P"_i^(i in 1..n)] space \{,
+    quad "m"_j^(j in 1..M),
     \},
     delim: "["
   ) $, [_generic definition_]),

report/chapters/03_theory/python_syntax.typ

@@ -26,7 +26,7 @@
 
 #let statements = (
   ($"t"$, [_expression_]),
-  ($"s"; "t"$, [_inline sequence_]),
+  ($"s"; "s"$, [_inline sequence_]),
   ($ cases(
     "s" #nl,
     "s",
@@ -36,14 +36,14 @@
   ($"x": "T"$, [_variable declaration_]),
   ($ cases(
     #syntax[def] f("x": "T") -> "T": #nl,
-    #tab "t" #nl,
+    #tab "s",
     delim: "["
   ) $, [_def_]),
   ($ cases(
     #syntax[if] "t": #nl,
     tab "s" #nl,
     #syntax[else]: #nl,
-    tab "s" #nl,
+    tab "s",
     delim: "["
   ) $, [_if / else_]),
   ($ cases(

report/chapters/04_implementation/01_overview.typ

@@ -5,7 +5,7 @@
 
 = Architecture Overview <sec:impl-overview>
 
-Our type checker is composed of several interdependent elements shown in @fig:architecture. At its core, there is a type registry which holds a list of all registered types. This registry is initialized with builtin types, like `float` and `str`, and can be further populated by user definitions written in the Midas language. Finally, it is used when type checking the Python source code based on the type checking rules we defined in @sec:theory-typing.
+Our type checker is composed of several interdependent elements shown in @fig:architecture. At its core, there is a types registry which holds a list of all registered types. This registry is initialized with builtin types, like `float` and `str`, and can be further populated by user definitions written in the Midas language. Finally, it is used when type checking the Python source code based on the type checking rules we defined in @sec:theory-typing.
 
 #figure(
   architecture.overview,

report/chapters/04_implementation/02_types.typ

@@ -12,7 +12,7 @@ In our type system, we will indeed have different kinds of types with different
 == Base Types <sec:types-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.
+For the special `tuple` type, we can define a more specific class which can hold each item's type. This will allow nice type checking of subscript expressions for example.
 
 #figure(
   ```python
@@ -50,7 +50,7 @@ A similar approach is used for constraint types, by embedding the base type and
 
 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:variance-inference.
 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.
+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.
 
@@ -83,7 +83,7 @@ A function type thus have a parameter specification and a return type. That para
 @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`.
+Finally, we will also define a structure to hold multiple signatures 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

report/chapters/04_implementation/03_registry.typ

@@ -4,7 +4,7 @@
 
 = Types Registry <sec:impl-registry>
 
-With structures to represent our types, we now need to implement the registry which hold all builtin and user-defined types, as well as named predicates. As a reminder of requirements given in @sec:impl-overview, the registry must also provide a method `is_subtype` to check whether according to our subtyping rules one type is subtype of another, a method to register a type with a name, a method to lookup a type given a name, and some methods to manipulate types, such as instantiating a generic type given some arguments. We will also registration and lookup methods for predicates, as well as for type members (defined in `extend` statements).
+With structures to represent our types, we now need to implement the registry which hold all builtin and user-defined types, as well as named predicates. As a reminder of requirements given in @sec:impl-overview, the registry must also provide a method `is_subtype` to check whether according to our subtyping rules one type is subtype of another, a method to register a type with a name, a method to lookup a type given a name, and some methods to manipulate types, such as instantiating a generic type given some arguments. We will also implement registration and lookup methods for predicates, as well as for type members (defined in `extend` statements).
 
 @fig:registry-contract shows the minimal contract our registry must satisfy.
 
@@ -31,7 +31,7 @@ With structures to represent our types, we now need to implement the registry wh
 
 The `define_*` and `lookup_*`/`get_*` methods are quite straightforward, inserting and querying an internal dictionary with some added safeguards and errors to prevent redefining an entity or handle undefined references. Additionally, `define_member` handles overriding methods by wrapping multiple method definitions with the same member name inside an `OverloadedFunction` type. This process is detailed in @sec:define_member hereafter. The complete implementation of `TypesRegistry` is available in the repository in #code-ref(<types-registry>, "midas/checker/registry.py")
 
-== `define_member` <sec:define_member>
+== Implementing `define_member` <sec:define_member>
 
 #figure(
   ```python
@@ -70,10 +70,10 @@ The `define_*` and `lookup_*`/`get_*` methods are quite straightforward, inserti
   caption: [Implementation of `TypesRegistry.define_member`]
 ) <fig:define_member>
 
-First in @fig:define_member:8, we retrieve the dictionary of all members defined for the given type, and check wether a member is already defined with the given name in @fig:define_member:9. If that is the case, we check whether the kind is equal; we avoid registering a method with the same name as a property and vice-versa. The current implementation simply ignores such definitions but an error could also be raised to be more explicit to the user.
-A second check in @fig:define_member:17 avoid redefining a member which is not a method (i.e. a property). If we are redefining a method, an `OverloadedFunction` is then built to combine already defined signatures with the new one, as implemented in @fig:define_member:24 to @fig:define_member:29.
+First in @fig:define_member:8, we retrieve the dictionary of all members defined for the given type, and check whether a member is already defined with the given name in @fig:define_member:9. If that is the case, we check whether the kind is equal; we avoid registering a method with the same name as a property and vice-versa. The current implementation simply ignores such definitions but an error could also be raised to be more explicit to the user.
+A second check in @fig:define_member:17 avoids redefining a member which is not a method (i.e. a property). If we are redefining a method, an `OverloadedFunction` is then built to combine already defined signatures with the new one, as implemented in @fig:define_member:24 to @fig:define_member:29.
 
-== `lookup_member`
+== Implementing `lookup_member`
 
 `lookup_member` also needs some logic to handle each kind ot types. Indeed, looking up a member on a type (e.g. when processing an attribute reference expression like `foo.bar`), it may be defined in any of the type's supertypes too. Thus the method needs to recurse in the hierarchy if the member cannot be found directly on the requested type.
 
@@ -127,9 +127,9 @@ A second check in @fig:define_member:17 avoid redefining a member which is not a
   caption: [Implementation of `TypesRegistry.lookup_member`]
 ) <fig:lookup_member>
 
-Because we defined our internal type representations with dataclasses, we can easily leverage Python's pattern-matching capabilities to handle each case, as shown in @fig:lookup_member. The method is also quite straightforward though two things can be noted. The first is that looking up a member on `UnknownType` returns `UnknownType`. This basically tells the registry to go along with any references to unknown types, trusting the user that what they are doing is correct. It also allows gracefully propagating errors to avoid early returns that could be caused by raising an exception. The second important part of `lookup_member` is how `AppliedType` is handled. Since this type is derived from a generic type, its members may contain type variables. These are substituted lazily when referenced, i.e. in this method. `substitute_typevars` is a method which performs this substitution recursively given a mapping of type parameters to concrete type arguments. Its implementation is available in the repository in #code-ref(<substitute_typevars>, "midas/checker/types.py").
+Because we defined our internal type representations with dataclasses, we can easily leverage Python's pattern-matching capabilities to handle each case, as shown in @fig:lookup_member. The method is also quite straightforward though two things can be noted. The first is that looking up a member on `UnknownType` returns `UnknownType`. This basically tells the registry to go along with any references to unknown types, trusting the user that what they are doing is correct. It also allows gracefully propagating errors to avoid early returns that could be caused by raising an exception. The second important part of `lookup_member` is how `AppliedType` is handled. Since this type is derived from a generic type, its members may contain type variables. These are substituted lazily when referenced, i.e. in this method. `substitute_typevars` is a function which performs this substitution recursively given a mapping of type parameters to concrete type arguments. Its implementation is available in the repository in #code-ref(<substitute_typevars>, "midas/checker/types.py").
 
-== `apply_generic`
+== Implementing `apply_generic`
 
 `apply_generic` is a simple method which builds an `AppliedType` from a `GenericType` and a list of type arguments. This method is used when processing expressions such as `Foo[Bar]` and is implemented using the aforementioned `substitute_typevars`. Moreover, it checks potential bounds of type parameters. It is also used for the special `TupleType` which is constructed as `tuple[Type1, Type2, ...]`, as shown in @fig:apply_generic.
 
@@ -185,7 +185,7 @@ The first case handling `DerivedType`, @fig:apply_generic:3 to @fig:apply_generi
 
 #pagebreak(weak: true)
 
-== `is_subtype` <sec:is_subtype>
+== Implementing `is_subtype` <sec:is_subtype>
 
 This method is one of the central parts of our type system. Its role is simple: judge, according to the rules we defined in @sec:typing-subtyping (and some we skipped), whether a given type (`type1`) should be considered a subtype of another (`type2`).
 
@@ -224,7 +224,7 @@ For builtin types, we define some hardcoded subtype relationships, which are che
   caption: [`is_subtype`: builtins and type variables]
 ) <fig:is_subtype-base-vars>
 
-Then we have two similar kinds of types. First, `DerivedType` which encode an explicit subtype relationship, and `ConstraintType` which contain a base type and a constraint. To check these, we simply call `is_subtype` on the base type recursively. The latter corresponds to #smallcaps[S-Constr] in @tab:typing-subtyping-constraint. Note that we only consider `type1`, and not `type2`. The reason we only recurse on the potential subtype is that we are checking whether `type2` is in the hierarchy _above_ `type1`, i.e. a supertype. Because we don't allow multiple inheritance, the type lattice is basically a tree (in the graph theory sense) and a supertype must be in the same branch. This recursion process is an application of #smallcaps[S-Trans] (see @tab:typing-subtyping-base), which should either converge at one of the simpler cases described above or converge at a negative result if the subtype relationship cannot be verified (i.e. not subtyping rule was matched).
+Then we have two similar kinds of types. First, `DerivedType` which encodes an explicit subtype relationship, and `ConstraintType` which contains a base type and a constraint. To check these, we simply call `is_subtype` on the base type recursively. The latter corresponds to #smallcaps[S-Constr] in @tab:typing-subtyping-constraint. Note that we only consider `type1`, and not `type2`. The reason we only recurse on the potential subtype is that we are checking whether `type2` is in the hierarchy _above_ `type1`, i.e. a supertype. Because we don't allow multiple inheritance, the type lattice is basically a tree (in the graph theory sense) and a supertype must be in the same branch. This recursion process is an application of #smallcaps[S-Trans] (see @tab:typing-subtyping-base), which should either converge at one of the simpler cases described above or converge at a negative result if the subtype relationship cannot be verified (i.e. not subtyping rule was matched).
 The implementation shown in @fig:is_subtype-derived-constr is a straightforward application of these rules.
 
 #codly(
@@ -237,7 +237,7 @@ The implementation shown in @fig:is_subtype-derived-constr is a straightforward
 ) <fig:is_subtype-derived-constr>
 
 Special care must be taken when comparing two `AppliedType`, that is, instances of generic types.
-For $"T"_1["A"_11, "A"_12, ...] <: "T"_2["A"_21, "A"_22, ...]$ to be true, $"T"_1$ and $"T"_2$ must first refer to the same generic type. If they are, we must then check that each pair of arguments $("A"_11, "A"_21), ("A"_12, "A"_22), ..$ respect the variance of corresponding type parameters. This means that for a given triplet $("A"_1, "A"_2, "P")$, where $"A"_1$ and $"A"_2$ are paired arguments of `type1` and `type2`, and $"P"$ is the matching type parameter of the generic type:
+For $"T"_1["A"_11, "A"_12, ...] <: "T"_2["A"_21, "A"_22, ...]$ to be true, $"T"_1$ and $"T"_2$ must first refer to the same generic type. If they do, we must then check that each pair of arguments $("A"_11, "A"_21), ("A"_12, "A"_22), ...$ respects the variance of corresponding type parameters. This means that for a given triplet $("A"_1, "A"_2, "P")$, where $"A"_1$ and $"A"_2$ are paired arguments of `type1` and `type2`, and $"P"$ is the matching type parameter of the generic type:
 - if $"P"$ is _covariant_, we must check that $"A"_1 <: "A"_2$
 - if $"P"$ is _contravariant_, we must check that $"A"_2 <: "A"_1$
 - if $"P"$ is _invariant_, we must check both conditions
@@ -261,7 +261,7 @@ Only three rules remain to check for dataframes, columns and most importantly fu
 Columns are simply regarded as invariant generic types. They are not implement using a regular `GenericType`/`AppliedType` because it makes many mechanisms much simpler to implement and reason about, especially regarding attributes and methods, which is worth making them a special construct.
 
 For dataframes, another approach is taken: structural subtyping. What this means in our type checker is that a dataframe is considered a subtype of another if it has at least the same columns (by name) as the supertype, and they are compatible (i.e. columns of `type1` are subtypes of `type2`'s). This idea has some benefits and drawbacks.
-Starting with the negative, allowing `type1` to have more columns than `type2` could have a runtime impact. For example, if a function iterates over the columns or applies an operation which is not compatible with one of the extra columns, runtime behavior would not match the type checker's expectations. On the other hand, this allows much more flexibility for users who can pass whole dataframe to function which only need a subset of columns.
+Starting with the negative, allowing `type1` to have more columns than `type2` could have a runtime impact. For example, if a function iterates over the columns or applies an operation which is not compatible with one of the extra columns, runtime behavior would not match the type checker's expectations. On the other hand, this allows much more flexibility for users who can pass a whole dataframe to functions which only need a subset of columns.
 A potential solution not explored in this work could be to add a dedicated type, construct or syntax for explicit structural subtyping.
 
 Finally, as shown in @fig:is_subtype-df-cols-funcs, functions are checked separately. Indeed, the algorithm as described in @tab:typing-subtyping-function and @app:function-subtyping is too complex to inline in this method. The implementation is discussed in @sec:is_func_subtype.
@@ -275,7 +275,7 @@ Finally, as shown in @fig:is_subtype-df-cols-funcs, functions are checked separa
   caption: [`is_subtype`: dataframes, columns and functions]
 ) <fig:is_subtype-df-cols-funcs>
 
-== `is_func_subtype` <sec:is_func_subtype>
+== Implementing `is_func_subtype` <sec:is_func_subtype>
 
 This section describes the implementation of the function subtyping verification algorithm. Please refer to @app:function-subtyping for more information on the underlying theory and formal rules.
 The complete implementation of `is_func_subtype` is given in @fig:is_func_subtype.

report/chapters/04_implementation/04_midas_language.typ

@@ -16,13 +16,13 @@ Processing a Midas definitions file is done in 3 steps:
 
 + typing, i.e. processing each statement, registering types and predicates in the registry
 
-Each of these steps map to a dedicated class, respectively `MidasLexer`, `MidasParser` and `MidasTyper`.
+Each of these steps maps to a dedicated class, respectively `MidasLexer`, `MidasParser` and `MidasTyper`.
 
-== Lexing and parsing <sec:midas-lexing-parsing>
+== Lexing and Parsing <sec:midas-lexing-parsing>
 
 The lexer and parser follow the structure presented by Nystrom@Nystrom2021 and implemented in #fn-link(<pebble-midas>, "https://git.kb28.ch/HEL/pebble", new: false)[pebble]@Pebble.
 
-Concretely, the lexer scans the source code character by character and produces tokens. Several token types are defined to cover all needs in Midas, such as operators, identifiers, keywords and punctuation. The full list of token types is included in @tab:token-types. Whitespace and comments are also converted to tokens but are ignored by the parser. Each token, as represented by the class shown in @fig:token-class, has a token type, a lexeme (i.e. the raw characters making up that token) and a position. That position is crucial for reporting diagnostics as it allows precisely showing the user where an error is in the source file. Tokens representing literals also contain their literal value, like strings, numbers and constants.
+Concretely, the lexer scans the source code character by character and produces tokens. Several token types are defined to cover all needs in Midas, such as operators, identifiers, keywords and punctuation. The full list of token types is included in @tab:token-types. Whitespace and comments are also converted to tokens but are ignored by the parser. Each token, as represented by the class shown in @fig:token-class, has a token type, a lexeme (i.e. the raw characters making up that token) and a position. That position is crucial for reporting diagnostics as it allows precisely showing the user where an error is in the source file. Tokens representing literals also contain their literal values, like strings, numbers and other constants.
 
 #figure(
   ```python
@@ -140,7 +140,7 @@ These tokens are then passed through the parser which builds an #acr("AST") show
 
 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 <sec:midas-interpretation>
+== Processing Statements <sec:midas-interpretation>
 
 Each statement is processed in order. In the following sections we will get in more details for each kind of statements, and look at how we can implement their effects on the types registry.
 
@@ -148,7 +148,7 @@ The complete implementation of `MidasTyper` is available in the project's reposi
 
 The basic members and methods referenced in implementations of this section are listed in @fig:midas-typer-members.
 
-=== Building types <sec:midas-building-types>
+=== Building Types <sec:midas-building-types>
 
 Before we can register a new type or an alias, we must be able to convert an #acr("AST") representation of a type into our internal type representation structures. For this we leverage the visitor pattern by implementing the visitor class of `Type` #acr("AST") nodes, as generated in @sec:midas-lexing-parsing. We thus make `MidasTyper` extend ```python m.Type.Visitor[Type]```#footnote[To avoid confusion between Midas and Python #acr("AST") nodes, their namespaces are imported as `m` and `p` respectively. A standalone reference to `Type` relates to the union of internal type representations mentioned in @sec:impl-types.]<fn:types-ref>, indicating that it must handle visiting any `m.Type` node and return a `Type` object.
 
@@ -172,7 +172,7 @@ As an example, visiting a `m.NamedType` node simply looks up the name in the reg
   caption: [Midas Typer: implementation of `visit_named_type`]
 ) <fig:midas-visit_named_type>
 
-Applied generics are built by looking up the type by its name, processing all arguments to build types and call `TypesRegistry.apply_generic`. The implementation shown in @fig:midas-visit_generic_type also handles the special `Column` type separately, as discussed in @sec:is_subtype.
+Applied generics are built by looking up the type by its name, processing all arguments to build types and calling `TypesRegistry.apply_generic`. The implementation shown in @fig:midas-visit_generic_type also handles the special `Column` type separately, as discussed in @sec:is_subtype.
 
 #figure(
   ```python
@@ -225,7 +225,7 @@ As you can see in the implementation above, in @fig:midas-visit_constraint_type,
 
 Processing functions and dataframe types is naturally implemented by processing their internal types (e.g. parameters, columns) and building the corresponding internal representations.
 
-=== Type checking expressions <sec:midas-checking-expr>
+=== Type Checking Expressions <sec:midas-checking-expr>
 
 The process of type checking constraint expressions (`m.Expr`) is nearly identical to type checking a Python expression. Thus, the implementation is quite similar. This will be covered in the section concerning `PythonTyper`, i.e. @sec:python-check-expr.
 For now, we only look at `visit_variable_expr` and `visit_wildcard_expr` which call `get_variable` to return the type of the referenced variable. This method is detailed in @fig:midas-typer-members and in essence does the following:
@@ -235,7 +235,7 @@ For now, we only look at `visit_variable_expr` and `visit_wildcard_expr` which c
 
 If all three lookups fail, `UnknownType` is returned and an error is reported.
 
-=== Alias statement <sec:midas-alias-stmt>
+=== Alias Statement <sec:midas-alias-stmt>
 
 Now that we can build types we must implement a way to register them for future reference.
 The first and simplest statement is the alias statement (`m.AliasStmt`). Its effect is to bind the given name to the type defined on the right-hand side. The implementation is quite straightforward, as demonstrated in @fig:midas-visit_alias_stmt. Do note that `self._current_name` is set before processing the `m.Type` node, and cleared afterwards, so that cyclic references can be caught. The exception raised by the registry is also caught and reported through an error diagnostic to continue processing remaining statements.
@@ -255,7 +255,7 @@ The first and simplest statement is the alias statement (`m.AliasStmt`). Its eff
   caption: [Midas Typer: implementation of `visit_alias_stmt`]
 ) <fig:midas-visit_alias_stmt>
 
-=== Type statement <sec:midas-type-stmt>
+=== Type Statement <sec:midas-type-stmt>
 
 Type statements work similarly to alias statements, though they wrap the defined type in a `DerivedType` or `GenericType` depending on whether there are parameters.
 Additionally, if parameters are given, they are processed and transformed into `TypeVar` instances, and registered in an internal `_local_variables` dictionary. This internal registry is used by `TypesRegistry.get_type` to resolve references to type variables inside generic types and `extend` statements.
@@ -293,7 +293,7 @@ Additionally, if parameters are given, they are processed and transformed into `
   caption: [Midas Typer: implementation of `visit_type_stmt`]
 ) <fig:midas-visit_type_stmt>
 
-=== Predicate statement <sec:midas-predicate-stmt>
+=== Predicate Statement <sec:midas-predicate-stmt>
 
 When processing a predicate definition, we first need to gather all parameters and register them internally in `self._predicate_params`. Then we type check the predicate body, i.e. a constraint expression (`m.Expr`). After this we process all parameter specifications using the same method as for function types. Before defining the predicate, we also check that the body's type is valid, i.e. a subtype of `bool` or a function which returns a valid predicate (in case of a partially applied predicate). Lastly, we build a complete function signature for the predicate, combining curried parameter specifications into functions returning functions, and insert it in the registry. If the predicate definition does not include any parameter specification, we mark it as an alias. This whole procedure is implemented as shown in @fig:midas-visit_predicate_stmt.
 
@@ -345,7 +345,7 @@ When processing a predicate definition, we first need to gather all parameters a
   caption: [Midas Typer: implementation of `visit_predicate_stmt`]
 ) <fig:midas-visit_predicate_stmt>
 
-=== Extend statement <sec:midas-extend-stmt>
+=== Extend Statement <sec:midas-extend-stmt>
 
 The last kind of statement available in our definition language is the `extend` statement. As explained in @sec:theory-syntax-midas, this allows defining members (properties and methods) on an already defined type. Processing it is rather straightforward, and comes down to two steps. First, we need to get the type being extended from the registry. The second step is simply iterating over each member statement and calling `TypesRegistry.define_member`. @fig:midas-visit_extend_stmt presents the short implementation of the method handling `extend`statements.
 
@@ -394,7 +394,7 @@ Continuing with our example from @fig:example-midas-ast, the type statement woul
   caption: [Midas Example: registered type#footnote[Location and position objects are omitted for readability]]
 ) <fig:example-midas-type>
 
-== Variance inference <sec:variance-inference>
+== Variance Inference <sec:variance-inference>
 
 The main `resolve` method of `MidasTyper`, as shown in @fig:midas-typer-resolve and @fig:midas-typer-members, first processes all statements, and then summons a `VarianceManager` to infer variance of all types.
 
@@ -435,7 +435,7 @@ When the generic type has been full walked, the tracker returns the list of type
 - otherwise it is *invariant*
 Its implementation is given in @fig:midas-variance-tracker.
 
-It should be noted that we also use a `VarianceManager` to orchestrate how all the types are processed. The naive approach is to simply iterate over each type and infer their variance. However, this breaks down when a type is referenced before it is processed, or even inside itself. To counter such situations, we introduce a queue of types currently being processed. When walking through a type, if we encounter an `AppliedType`, we first check whether it is in the queue. If not, we ask the manager to infer its variance before continuing, as highlighted in @fig:midas-variance-inferrer-walk:42 to @fig:midas-variance-inferrer-walk:47.
+It should be noted that we also use a `VarianceManager` to orchestrate how all the types are processed. The naive approach is to simply iterate over each type and infer its variance. However, this breaks down when a type is referenced before it has been processed, or even inside itself. To counter such situations, we introduce a queue of types currently being processed. When walking through a type, if we encounter an `AppliedType`, we first check whether it is in the queue. If not, we ask the manager to infer its variance before continuing, as highlighted in @fig:midas-variance-inferrer-walk:42 to @fig:midas-variance-inferrer-walk:47.
 
 `VarianceManager` is a simple helper class. Its main method, `infer`, is shown in @fig:midas-variance-manager-infer.
 

report/chapters/04_implementation/05_python_checking.typ

@@ -9,7 +9,7 @@
 
 = Python Type Checking <sec:impl-python>
 
-We have now built a type definition language and registry, but it is of no use if we cannot type-check our Python code. In a similar fashion to `MidasTyper`, we must now implement a `PythonTyper`. Its role is to take in some Python source code and the types registry, walk through each statement and expression, infer the type of each term and verify the program's soundness. We will need several tools to concretize this process, such as a resolver to keep track of which value each variable references, and an environment to store the inferred types of local variables.
+We have now built a type definition language and registry, but it is of no use if we cannot type check our Python code. In a similar fashion to `MidasTyper`, we must now implement a `PythonTyper`. Its role is to take in some Python source code and the types registry, walk through each statement and expression, infer the type of each term and verify the program's soundness. We will need several tools to concretize this process, such as a resolver to keep track of which value each variable references, and an environment to store the inferred types of local variables.
 
 For the sake of readability and conciseness, many parts of the implementation will be omitted from the following sections, focusing instead on the basic principles and most interesting methods. As always, the full source code is available in the repository, mainly in #code-ref(<checker>, "midas/checker").
 
@@ -99,7 +99,7 @@ More generally, if all sub-branches assign to a variable, we can consider it def
 
 == Environments <sec:python-env>
 
-While type checking, we will need to record what each variable's type is, much like `Gamma` in formal typing rule definitions (see @sec:theory-typing). This leads to the implementation of an `Environment` class, as presented by Nystrom in chapter 8.3 of _Crafting Interpreters_@Nystrom2021. Mirroring `Resolver`'s scopes, environments are nested into one another to isolate code blocks. The main difference with Nystrom's `Environment` class is that ours will store types rather than values. Additionally, as demonstrated in @sec:python-returns, `Environment` is also responsible for keeping track of possible return types in the associated scope.
+While type checking, we will need to record what each variable's type is, much like $Gamma$ in formal typing rule definitions (see @sec:theory-typing). This leads to the implementation of an `Environment` class, as presented by Nystrom in chapter 8.3 of _Crafting Interpreters_@Nystrom2021. Mirroring `Resolver`'s scopes, environments are nested into one another to isolate code blocks. The main difference with Nystrom's `Environment` class is that ours will store types rather than values. Additionally, as demonstrated in @sec:python-returns, `Environment` is also responsible for keeping track of possible return types in the associated scope.
 
 We also define a special `Preamble` environment which contains bindings for global variables in the Python language, such as builtin functions and type constructors.
 
@@ -110,7 +110,7 @@ The source code for `Environment` and `Preamble` is available in the repository
 We now have the tools to start type checking our Python code.
 The input given to `PythonTyper` is basically a sequence of statements (`p.Stmt`). Using the visitor pattern, we make `PythonTyper` extend ```python p.Stmt.Visitor[None]``` and implement all `visit_*_stmt` methods.
 
-=== Variable assignment <sec:python-var-assign>
+=== Variable Assignment <sec:python-var-assign>
 
 One of the main mechanics manipulating the environment is variable declaration and assignment.
 During parsing, a statement such as ```python foo: int = 3```, represented in Python as a single `ast.AnnAssign` node, is split into two #acr("AST") nodes. The first is a type assignment (`p.TypeAssign`), which declares a new variable with the given type. The second is a variable assignment (`p.AssignStmt`). Implementing `visit_type_assign` is straightforward: we first resolve the type annotation expression and then define a new variable in the current environment, as demonstrated in @fig:python-visit_type_assign.
@@ -170,14 +170,14 @@ Handling the variable assignment part is a bit more involved, because Python (an
   caption: [Python Typer: implementation of `visit_assign_stmt` (variable target)]
 ) <fig:python-visit_assign_stmt>
 
-This is also one of the places our subtyping rules come into play. When assigning to an already defined variable, we check that the value's type is a subtype of the variable's type.#footnote[`PythonTyper.is_subtype` is simply a shortcut for calling `is_subtype` on the types registry], emitting an error diagnostics in case of incompatibility.
+This is also one of the places our subtyping rules come into play. When assigning to an already defined variable, we check that the value's type is a subtype of the variable's type.#footnote[`PythonTyper.is_subtype` is simply a shortcut for calling `is_subtype` on the types registry], emitting an error diagnostic in case of incompatibility.
 
 === Returns <sec:python-returns>
 
 One special control flow statement is the ```py return``` keyword.
 Its effect is twofold. First, it cuts a branch short and any further statement in that branch is skipped. Secondly, it provides a possible return type for the parent function. The latter implies that return statements must appear inside functions.
 
-To easily implement the first effect, we will take advantage of exceptions and raise one inside `visit_return_stmt` (named `ReturnException`). We must then catch this exception at the closest branching point, i.e. the entry point of a block. In our case, in addition to a method type checking a single statement (`process_stmt`), we can implement a method to type check a whole block (`process_block`). Inside the latter we can then wrap calls `process_stmt` in a `try`/`except` statement. If a `ReturnException` is caught while processing a block and some statements remain to be processed, we can emit a warning to the user indicating that they will be skipped at runtime.
+To easily implement the first effect, we will take advantage of exceptions and raise one inside `visit_return_stmt` (named `ReturnException`). We must then catch this exception at the closest branching point, i.e. the entry point of a block. In our case, in addition to a method type checking a single statement (`process_stmt`), we can implement a method to type check a whole block (`process_block`). Inside the latter we can then wrap calls to `process_stmt` in a `try`/`except` statement. If a `ReturnException` is caught while processing a block and some statements remain to be processed, we can emit a warning to the user indicating that they will be skipped at runtime.
 
 @fig:python-visit_return_stmt shows how the exception is raised while @fig:python-process_block shows how the exception is caught.
 
@@ -238,7 +238,7 @@ Similarly to how we handled variable assignments in `if` branches (see @fig:reso
   caption: [Python Typer: implementation of `visit_if_stmt`]
 ) <fig:python-visit_if_stmt>
 
-=== Function definitions <sec:python-functions>
+=== Function Definitions <sec:python-functions>
 
 Function definitions include many components from all kinds of parameters, default values return type hints and their bodies. One particular property is the optionality of return type hints and the potential multiplicity of return statements inside a function body.
 What we want for our type checker is to ensure soundness of return types while helping the user by giving them as much freedom as possible by inferring types where not explicitly given.
@@ -270,7 +270,7 @@ The complete implementation of `PythonTyper.visit_function` is listed in @fig:py
 
 == Type Checking Expressions <sec:python-check-expr>
 
-We extend `PythonTyper` to also type check expressions by inheriting ```python p.Expr.Visitor[Type]``` and implementing `visit_*_expr` methods. We thus make all expression visitor methods return a `Type` instance. Indeed, each Python expression is a typeable element composed into other expressions or statements. Some expressions such as literal value are trivial to type check whilst others can be much more complex. The latter are detailed in separate sections.
+We extend `PythonTyper` to also type check expressions by inheriting ```python p.Expr.Visitor[Type]``` and implementing `visit_*_expr` methods. We thus make all expression visitor methods return a `Type` instance. Indeed, each Python expression is a typeable element composed into other expressions or statements. Some expressions such as literal values are trivial to type check whilst others can be much more complex. The latter are detailed in separate sections.
 
 === Literals <sec:python-check-literals>
 
@@ -292,7 +292,7 @@ Applying typing rules for literals (@tab:typing-literals) is only a matter of ma
   caption: [Python Typer: implementation of `visit_literal_expr`]
 ) <fig:python-visit_literal_expr>
 
-For literal list expressions, we will reuse `TypesRegistry.reduce_types` method used in @fig:python-function-return-type to try and find a supertype of all item types.
+For literal list expressions, we will reuse the `TypesRegistry.reduce_types` method used in @fig:python-function-return-type to try and find a supertype of all item types.
 
 #figure(
   ```python
@@ -321,7 +321,7 @@ Literal dictionaries are handled in the same manner, finding a supertype for key
 
 In Python, builtin operators are implemented through _dunder-methods_, i.e. methods on the operands. To the eyes of the type checker, an operation is thus equivalent to a function call. We can implement this idea by following these steps:
 + Get the dunder-method name corresponding to the operator
-+ Type-check all operands (two for binary operators, one for unary operators)
++ Type check all operands (two for binary operators, one for unary operators)
 + Lookup the method on the left operand#footnote[Reverse operations (e.g. `__radd__`) have not been implemented in Midas yet]
 + Type check a call to the method with the given operand(s)
 
@@ -336,7 +336,7 @@ Similarly, subscripts are de-sugared into calls to `__getitem__`.
 
 Function calls are not always as straightforward as matching arguments with parameters and getting the return type. For a start, the callee is not necessary a direct `Function`. It may be a `DerivedType` or an `AppliedType`, in which case we must _unfold_ the type hierarchy to get the actual function type. It may also be an `OverloadedFunction`, in which case we must resolve which overload to call. It can also be a `GenericType`, in which case we must try and resolve the actual type arguments based on usage. To keep the type checker tidy, we introduce a separate `CallDispatcher` class, which we can reuse in `MidasTyper` for call expressions too.
 
-This dispatcher has one main entrypoint: `get_result`. This method, shown in @fig:dispatcher-get_result-signature, takes in a callee type, positional and keyword arguments, and returns a `CallResult` object. This object bundles information about the result type and potential error should the dispatcher fail to resolve the call. The complete methods discusses hereafter are included in @fig:call-dispatcher. Their implementations are available in the repository in #code-ref(<call-dispatcher>, "midas/checker/dispatcher.py").
+This dispatcher has one main entrypoint: `get_result`. This method, shown in @fig:dispatcher-get_result-signature, takes in a callee type, positional and keyword arguments, and returns a `CallResult` object. This object bundles information about the result type and potential error, should the dispatcher fail to resolve the call. The complete methods discussed hereafter are included in @fig:call-dispatcher. Their implementations are available in the repository in #code-ref(<call-dispatcher>, "midas/checker/dispatcher.py").
 
 #figure(
   ```python
@@ -370,7 +370,7 @@ This dispatcher has one main entrypoint: `get_result`. This method, shown in @fi
 
 `CallDispatcher` is generic in `E`, which represents an expression base class. This allows instantiating it both for `m.Expr` and `p.Expr`.
 
-The simple case where the callee is a `Function` involves matching call-site arguments with parameters in the function's specification. Then, if a match is possible each pair is check for correct typing. Similar to variable assignment (#smallcaps[T-Assign], see @sec:python-var-assign), an argument must be of the same type as the parameter it matches with (module subsumption). Pragmatically, this corresponds to @fig:dispatcher-match-func.
+The simple case where the callee is a `Function` involves matching call-site arguments with parameters in the function's specification. Then, if a match is possible, each pair is checked for correct typing. Similar to variable assignment (#smallcaps[T-Assign], see @sec:python-var-assign), an argument must be of the same type as the parameter it matches with (modulo subsumption). Pragmatically, this corresponds to @fig:dispatcher-match-func.
 
 #codly(
   range: (14, 24),
@@ -462,7 +462,7 @@ Now that we have a method to choose an overload given some arguments, we can add
   caption: [Call Dispatcher: call to `OverloadedFunction`]
 ) <fig:dispatcher-match-overloaded>
 
-=== Generic function <sec:python-call-generic>
+=== Generic Function <sec:python-call-generic>
 
 Generic functions are useful for defining some kind of template behavior while allowing different types to be used. However, when it comes to a call to such a function, things get a bit more complicated. Indeed, type parameters must be mapped to concrete types and unified depending on the actual call-site arguments before getting the return type. Taking the example of a simple generic doubling function ```py def double(value: T) -> T```, the return type depends on the type of the argument. Furthermore, in a more complex case like ```py def add(v1: T, v2: T) -> T```, the type variable `T` must be mapped to the same type for both `v1` and `v2`.
 This process is covered more in depth in chapter 22 of #acr("TaPL")@tapl.
@@ -483,7 +483,7 @@ Using this class, we can complete `get_result` with the last case handling calls
 
 == Casts and Static Evaluation <sec:python-check-casts>
 
-From a type checking point of view, cast expressions are trivial to implement by applying #smallcaps[T-Cast]. `visit_cast_expr` simply returns the type passed to `cast`. There is however a fundamental premise making casts sounds, that is, the expression must conform to the given type. Most of the time, users will use cast expressions when the expression is not properly typeable at compile-time, but will always be valid at runtime. To maintain type safety, we will thus generate a runtime assertion checking that premise (see @sec:gen-assertions). However, these check might be quite computationally expensive, so we will provide users with an unsafe alternative that does not produce any runtime verification, `unsafe_cast`.
+From a type checking point of view, cast expressions are trivial to implement by applying #smallcaps[T-Cast]. `visit_cast_expr` simply returns the type passed to `cast`. There is however a fundamental premise making casts sounds, that is, the expression must conform to the given type. Most of the time, users will use cast expressions when the expression is not properly typeable at compile-time, but will always be valid at runtime. To maintain type safety, we will thus generate a runtime assertion checking that premise (see @sec:gen-assertions). Still, these checks might be quite computationally expensive, so we will provide users with an unsafe alternative that does not produce any runtime verification, `unsafe_cast`.
 
 Additionally, there is a particular category of expressions which can be checked statically to verify whether the cast expression is valid. These are all literal values. For example, given a ```midas type Positive = float where _ >= 0```, an expression such as ```py cast(Positive, -12.3)``` can be fully rejected at compile-time. Implementing such a verification is not as simple as it may seem, as it implies we must first extract the literal Python value from the #acr("AST") representation and _evaluate_ the cast. @fig:python-visit_cast_expr shows the full method type checking casts.
 
@@ -506,11 +506,11 @@ Additionally, there is a particular category of expressions which can be checked
 
 === Static Evaluator <sec:python-evaluator>
 
-Most interestingly in the evaluation process is how to handle constraint types. In addition to checking compliance with the base type, the literal value must also fit the constraint expression, which means _evaluating_ the expression to a boolean. For this purpose we introduce a dedicate `Evaluator` class.
+Most interestingly in the evaluation process is how to handle constraint types. In addition to checking compliance with the base type, the literal value must also fit the constraint expression, which means _evaluating_ the expression to a boolean. For this purpose we introduce a dedicated `Evaluator` class.
 Our constraint evaluator implements `m.Expr.Visitor[Any]`, accepting any expression and returning a final value.
-Another solution could have been to let the expression be interpreted by Python, using ```py exec``` or a similar function, but our constraint syntax is quite limited and slightly different, it seemed more practical to implement our own interpreter. This also allows sand-boxing the environment to the context we want and handle calls to other predicate functions.
+Another solution could have been to let the expression be interpreted by Python, using ```py exec``` or a similar function, but our constraint syntax being quite limited and slightly different, it seemed more practical to implement our own interpreter. This also allows sand-boxing the environment to the context we want and handle calls to other predicate functions.
 
-The implementation is no so interesting (basically applying operators, getting attributes with `getattr`, etc.). The complete source code is available in the repository in #code-ref(<evaluator>, "midas/checker/evaluator.py").
+The implementation is not so interesting (basically applying operators, getting attributes with `getattr`, etc.). The complete source code is available in the repository in #code-ref(<evaluator>, "midas/checker/evaluator.py").
 
 One particularity of Midas is how it allows curried application of predicates. Given the example in @fig:example-curried-application, we see that the first call results in a partially applied predicate function, while the second evaluates to a boolean.
 
@@ -562,19 +562,19 @@ In practice, we keep track of a scope dictionary containing all defined variable
 
 == Frames and Columns <sec:python-df-cols>
 
-There is still one big part of the type checker that we have not covered: dataframes and columns. Properly type checking dataframe operations is a never-ending rabbit hole. Libraries like `pandas` or `polars` provide a enormous amount of features, as methods and syntax sugars. They also have highly polymorphic functions, accepting operations with all kinds of values, such as multiplying a dataframe by a scalar, a list, a column or even another dataframe. The results of these operations may vary quite a lot depending on the operands, or sometimes on the parameters passed to some functions. As discussed in @chap:state-of-the-art, some libraries do try and make developers' lives a little better by providing some static type-checking like #fn-link(<strictly-typed-pandas-py>, "https://strictly-typed-pandas.readthedocs.io")[_Strictly Typed Pandas_], or runtime schema verification like #fn-link(<pandera-py>, "https://pandera.readthedocs.io")[_Pandera_]@niels_bantilan-proc-scipy-2020.
+There is still one big part of the type checker that we have not covered: dataframes and columns. Properly type checking dataframe operations is a never-ending rabbit hole. Libraries like `pandas` or `polars` provide a enormous amount of features, as methods and syntax sugars. They also have highly polymorphic functions, accepting operations with all kinds of values, such as multiplying a dataframe by a scalar, a list, a column or even another dataframe. The results of these operations may vary quite a lot depending on the operands, or sometimes on the parameters passed to some functions. As discussed in @chap:state-of-the-art, some libraries do try and make developers' lives a little better by providing some static type checking like #fn-link(<strictly-typed-pandas-py>, "https://strictly-typed-pandas.readthedocs.io")[_Strictly Typed Pandas_], or runtime schema verification like #fn-link(<pandera-py>, "https://pandera.readthedocs.io")[_Pandera_]@niels_bantilan-proc-scipy-2020.
 
-Midas stands in between by providing some static type-checking for dataframe schemas and operations as well as generating runtime checks when a value is cast to such a type.
-We will explore in this section how we can not only provide type-checking for frame columns, for either accessing or assigning to them, but also handle some method calls with best effort inference of the resulting type.
+Midas stands in between by providing some static type checking for dataframe schemas and operations as well as generating runtime checks when a value is cast to such a type.
+We will explore in this section how we can not only provide type checking for frame columns, for either accessing or assigning to them, but also handle some method calls with best effort inference of the resulting type.
 
 #pagebreak(weak: true)
 
 === Schema Manipulation <sec:python-df-manager>
 
-When `PythonTyper` encounters a `p.SubscriptExpr` where the object is a `DataFrameType`, either in a getter context or in an assignment, we defer the resolution to a dedicated `FrameManager` class. This manager's responsibility is to check that referenced columns exist in the schema (and return their types). When assigning to a dataframe, it also build a modified version of the schema to include new columns.
+When `PythonTyper` encounters a `p.SubscriptExpr` where the object is a `DataFrameType`, either in a getter context or in an assignment, we defer the resolution to a dedicated `FrameManager` class. This manager's responsibility is to check that referenced columns exist in the schema (and return their types). When assigning to a dataframe, it also builds a modified version of the schema to include new columns.
 
 Method calls, caught in `PythonTyper` and forwarded to the manager, are handled by another class: `FrameMethodRegistry`.
-These classes allow a better separation of concern and a parallel implementation for frame and column types. Indeed, we will also implement a `ColumnManager` and a `ColumnMethodRegistry`.
+These classes allow a better separation of concerns and parallel implementations for frame and column types. Indeed, we will also create a `ColumnManager` and a `ColumnMethodRegistry`.
 
 === Method Registries <sec:python-df-methods>
 
@@ -632,20 +632,20 @@ When adding two columns together, we proceed in a similar way by looking up the
 Lastly, we must consider one particular edge case. Since columns can come from various places, they are not guaranteed to contain the same number of items. For `pandas` in particular, whenever a column or dataframe is used with another, the shortest is padded with nulls to match the longest length. This can lead to unexpected results which are totally hidden to the type checker. To counter such side-effects, we will enforce the condition that both operands must have the same length, through a runtime assertion.\
 Using the resulting schema, we build an ad-hoc `Function` which is passed to `CallDispatcher`. This allows reporting useful diagnostics for invalid arguments and reuses the machinery we already put in place for function calls. In our example, the function signature would be `fn(other: Any) -> Frame[a: float, b: <Unknown>, c: <Unknown>]`.
 
-The second kind of methods we will handle is slightly more complex. Aggregation methods act column-wise and perform operations between the all the values of the same column, reducing it to a scalar. For dataframes, aggregation may result in a series of scalars (one for each column) or a single scalar value. For the scope of this project, direct aggregation on raw dataframes will result in a top type. This does not mean that we cannot type check _some_ aggregations however.
+The second kind of methods we will handle is slightly more complex. Aggregation methods act column-wise and perform operations between all values of the same column, reducing it to a scalar. For dataframes, aggregation may result in a series of scalars (one for each column) or a single scalar value. For the scope of this project, direct aggregation on raw dataframes will result in a top type. This does not mean that we cannot type check _some_ aggregations however.
 
 Column aggregation does have a pretty stable and predictable output. Taking the example of the `mean` method, we do know that the mean of a series of number is computed by adding them together and dividing the total by the count. Fortunately, addition and division are both simple builtin operations that we already type check. We can thus define a formula, as a function of the column's item type, which "computes" the result type. For the `mean` method, this formula is ```py lambda t: ((t, "__add__", t), "__truediv__", "int")```, or more formally, $("T" + "T") \/"int"$#footnote[This formula does make the assumption that $"T" + "T"$ results in the same type as $"T" + "T" + ... + "T"$].
 
 Some other aggregation methods have even simpler formulae, such as ```py median = lambda t: t```, but some may not be represented in this form, such as the `std` or `kurtosis` methods. These simply return a top type.
 
-One last important construct that Midas supports is the `groupby` method. This method allows partitioning a column or dataframe in groups, according to some criteria, and compute some aggregations on each one. Recall @sec:types-dataframes where we defined special type kinds `FrameGroupBy` and `ColumnGroupBy`. We now use them as results of `DataFrameType.groupby` and `ColumnType.groupby` respectively, and implement dedicated method registries for each one. Their methods only include aggregation methods. This time, we can properly implement them for dataframes, because type-checking an aggregation method on a `FrameGroupBy` is equivalent to type-checking the method on `ColumnGroupBy` instances of each column, combining the result in a new `DataFrameType`. The actual type-checking computation is thus deferred to the other registry for `ColumnGroupBy` methods.
+One last important construct that Midas supports is the `groupby` method. This method allows partitioning a column or dataframe in groups, according to some criteria, and compute some aggregations on each one. Recall @sec:types-dataframes where we defined special type kinds `FrameGroupBy` and `ColumnGroupBy`. We now use them as results of `DataFrameType.groupby` and `ColumnType.groupby` respectively, and implement dedicated method registries for each one. Their methods only include aggregation methods. This time, we can properly implement them for dataframes, because type checking an aggregation method on a `FrameGroupBy` is equivalent to type checking the method on `ColumnGroupBy` instances of each column, combining the result in a new `DataFrameType`. The actual type checking computation is thus deferred to the other registry for `ColumnGroupBy` methods.
 In turn this registry simply delegates to `ColumnMethodRegistry`.
 
 All implementations of the classes discussed in this section are available in the repository in #code-ref(<df-methods>, "midas/checker/frames/").
 
 == Output <sec:python-output>
 
-We have finally finished implementing our type checker for Python. Although this report skips some parts of the implementation, most of the important areas are covered. Now while type-checking, we generated a number of diagnostics (warning or errors) which can be printed to the user. This is the job of the #acr("CLI"), which we will not discuss here but is available in the repository in #code-ref(<cli>, "midas/cli/"). Also checkout the #code-ref(<manual>, "docs/manual.pdf", body: [manual]) which provides detailed explanation of all #acr("CLI") functionalities.
+We have finally finished implementing our type checker for Python. Although this report skips some parts of the implementation, most of the important areas are covered. Now while type checking, we generated a number of diagnostics (warnings or errors) which can be printed to the user. This is the job of the #acr("CLI"), which we will not discuss here but is available in the repository in #code-ref(<cli>, "midas/cli/"). Also checkout the #code-ref(<manual>, "docs/manual.pdf", body: [manual]) which provides detailed explanations of all #acr("CLI") functionalities.
 
 There is still one missing part which we will discuss in @sec:impl-generation to generate the runnable Python code, including any necessary runtime assertions.
 Our type checker must then output some information about what it checked and the potential assertions to generate, as for ensuring that two dataframes have the same length.

report/chapters/04_implementation/06_generation.typ

@@ -12,7 +12,7 @@ This process comes after type checking, which verified the program's soundness a
 
 As Midas provides its own language to define custom types, the Python interpreter and other type checkers are completely oblivious to their existence and meaning. Although theoretically not necessary for runtime, types may be used while interpreting annotations, cast calls or through reflection. One solution is to generate stubs that can be used in Python code representing custom types defined in Midas.
 
-Simple derived types are translated through class inheritance, type aliases using simple assignments, and generics with Python native `Generic` and `TypeVar` classes. Functions are converted to `Protocol` subclasses for rich structural subtyping with other type checkers.
+Simple derived types are translated through class inheritance, type aliases using simple assignments, and generics with Python's native `Generic` and `TypeVar` classes. Functions are converted to `Protocol` subclasses for rich structural subtyping with other type checkers.
 Obviously, not all features of Midas can be translated into Python. Constraint types for example are simply represented like derived types, omitting the constraint aspect.
 
 The stubs can be manually generated with a #acr("CLI") command, to use when developing, and are automatically output when compiling for runtime use.

report/chapters/05_results_discussion.typ

@@ -16,11 +16,11 @@ In @chap:theory and @chap:impl, we have theorized and implemented a complete typ
 
 This is more than enough to make Midas usable in a wide range of contexts, including data science. The following sections demonstrate how Midas can be used to provide powerful type checking, both statically and at runtime.
 
-== Weather pipeline example <sec:results-pipeline>
+== Weather Pipeline Example <sec:results-pipeline>
 
 As an example, we will consider a sample weather-data transformation pipeline as shown in @app:example-pipeline, also available in the repository in #code-ref(<example-pipeline>, "examples/02_demonstration/weather/").
 
-=== Domain specific types <sec:pipeline-types>
+=== Domain Specific Types <sec:pipeline-types>
 
 Using the Midas language, we are able to define domain-specific types, as demonstrated in @fig:pipeline-base-types.
 
@@ -59,9 +59,9 @@ Finally, we can concisely define frame schemas that will become useful when mani
 
 #pagebreak(weak: true)
 
-=== Type checking in action <sec:pipeline-type-checking>
+=== Type Checking in Action <sec:pipeline-type-checking>
 
-Now what is the time for Midas to shine. The first step in a transformation pipeline is load some data. We will used `pandas` to read a dataframe from a #acr("CSV") file. Now, the compiler or type checker has no idea what this #acr("CSV") file might look like. Even if we specify a schema, there is no guarantee that the runtime file will conform to it. At most, the type checker can say that the result of `read_csv` is a dataframe. We thus introduce a `cast` expression to actually tell the type checker what the dataframe contains. Furthermore, a runtime assertion will check that the value returned by `read_csv` does indeed match our expectations.
+Now is the time for Midas to shine. The first step in a transformation pipeline is to load some data. We will use `pandas` to read a dataframe from a #acr("CSV") file. Now, the compiler or type checker has no idea what this #acr("CSV") file might look like. Even if we specify a schema, there is no guarantee that the runtime file will conform to it. At most, the type checker can say that the result of `read_csv` is a dataframe. We thus introduce a `cast` expression to actually tell the type checker what the dataframe contains. Furthermore, a runtime assertion will check that the value returned by `read_csv` does indeed match our expectations.
 Our load function thus looks like @fig:pipeline-load.
 
 #codly(
@@ -98,7 +98,7 @@ The second issue, which is more of a possible optimization, is the fact that `ca
 
 #pagebreak(weak: true)
 
-As implemented in @sec:python-df-methods, Midas will type check many operations on dataframes and columns, including `groupby` and aggregation methods. The result the computation shown in @fig:pipeline-aggregation is already typed as a dataframe of `float` columns by the type checker. We only add a `cast` to bring back our domain specific types, while re-checking value constraints. This latter point reveals one great feature missing from Midas: constraint unification (this will be discussed in @chap:conclusion).
+As implemented in @sec:python-df-methods, Midas will type check many operations on dataframes and columns, including `groupby` and aggregation methods. The result of the computation shown in @fig:pipeline-aggregation is already typed as a dataframe of `float` columns by the type checker. We only add a `cast` to bring back our domain specific types, while re-checking value constraints. This latter point reveals one great feature missing from Midas: constraint unification (this will be discussed in @chap:conclusion).
 
 #codly(
   range: (40, 53),
@@ -109,7 +109,7 @@ As implemented in @sec:python-df-methods, Midas will type check many operations
   caption: [Example Pipeline: data aggregation]
 ) <fig:pipeline-aggregation>
 
-Finally, there are some cases where Midas is not capable of properly type-checking some expressions, either by choice of the user or because some syntax is not yet supported. In either case, the type checker will gracefully handle untyped values by propagating them as `UnknownType`. Not only is `UnknownType` a top-type, it will also accept any operation, attribute or subscript access, etc.
+Finally, there are some cases where Midas is not capable of properly type checking some expressions, either by choice of the user or because some syntax is not yet supported. In either case, the type checker will gracefully handle untyped values by propagating them as `UnknownType`. Not only is `UnknownType` a top-type, it will also accept any operation, attribute or subscript access, etc.
 
 Moreover, users may want to cast an expression to a type but cannot afford the cost of checking it at runtime or feel it is too redundant with a previous known typing judgment. Alternatively, they may want to use a value with an unknown type which _behaves_ as another for all practical purposes (e.g. `np.float32`). In that case, they can use an escape hatch with `unsafe_cast` which blindly accepts that the given expression is of the specified type, as used in @fig:pipeline-plot.
 
@@ -124,7 +124,7 @@ Moreover, users may want to cast an expression to a type but cannot afford the c
 
 #pagebreak(weak: true)
 
-== Type errors <sec:results-errors>
+== Type Errors <sec:results-errors>
 
 In the previous section, we focused on dataframe operations, casts and runtime type errors, but Midas also catches static type errors. One classical but sneaky kind of error is mixing incompatible units. While using millimeters instead of centimeters when 3D-printing a pen holder might be comical, mixing monetary currencies while handling enterprise assets will probably get you fired. As demonstrated in @fig:caught-errors, Midas can help you avoid this kind of errors that can happen when some values share the same base representation (`float`).
 

report/chapters/06_conclusion.typ

@@ -5,9 +5,9 @@
 
 = Conclusion <chap:conclusion>
 
-This chapter concludes our exploration of Midas. We have seen how to define some formal typing rules to create a stricter static type system for Python. We then developed a custom language to define custom types, including dependent types with value constraints. We implemented a parser for this language from scratch, following Nystrom's _Crafting Interpreters_@Nystrom2021 and adapting a previous Python implementation of such an interpreter, #fn-link(<pebble-conclusion>, "https://git.kb28.ch/HEL/pebble")[pebble]@Pebble, written by the student. We developed a type registry to store builtin and user-defined types as dataclasses. Then, we implemented a complete type checker which is capable of processing an important subset of Python, performing some definite assignment analysis, enforcing our formal typing and subtyping rules and reporting useful contextualized diagnostics to the user. It also provides some powerful type checking of dataframe schemas and operations, including data aggregations. Finally, we implemented a code generator which converts cast expressions into runtime assertions verifying dependent type constraints and other premises that cannot be checked statically.
+This chapter concludes our exploration of Midas. We have seen how to define some formal typing rules to create a stricter static type system for Python. We then developed a custom language to define custom types, including dependent types with value constraints. We implemented a parser for this language from scratch, following Nystrom's _Crafting Interpreters_@Nystrom2021 and adapting a previous Python implementation of such an interpreter, #fn-link(<pebble-conclusion>, "https://git.kb28.ch/HEL/pebble")[pebble]@Pebble, written by the student. We developed a types registry to store builtin and user-defined types as dataclasses. Then, we implemented a complete type checker which is capable of processing an important subset of Python, performing some definite assignment analysis, enforcing our formal typing and subtyping rules, and reporting useful contextualized diagnostics to the user. It also provides some powerful type checking of dataframe schemas and operations, including data aggregations. Finally, we implemented a code generator which converts cast expressions into runtime assertions verifying dependent type constraints and other premises that cannot be checked statically.
 
-Reflecting on our initial objectives, we successfully created a type system on top of Python's type hints. It can detect many simple and complex type errors and generate runtime assertions when static checking is not sufficient. Midas respects Python's dynamic typing philosophy and leaves users free to annotate any amount of their code. Constraint types offer a flexible expression language to cover many use cases, from simple float value domain to calling builtin function or accessing object attributes.
+Reflecting on our initial objectives, we successfully created a type system on top of Python's type hints. It can detect many simple and complex type errors and generate runtime assertions when static checking is not sufficient. Midas respects Python's dynamic typing philosophy and leaves users free to annotate any amount of their code. Constraint types offer a flexible expression language to cover many use cases, from simple float value domain to calling builtin functions or accessing object attributes.
 
 By leveraging the visitor pattern in the parsers and type checkers, Midas is also easy to extend. Adding support for more Python constructs is only a matter of parsing it into a dedicated #acr("AST") node and implementing visitor methods where necessary. Classes such as `CallDispatcher`, `TypesRegistry` and `Resolver` clearly separate concerns and help organize the complex architecture of our system.
 
@@ -18,7 +18,7 @@ A non-exhaustive list of such opportunities and ideas has been compiled and orga
 
 === Current Limitations <sec:current-limitations>
 
-There are a few known limitations and unwanted behaviors in the current version of Midas. The first, which has already been discussed in @sec:gen-assertions, concerns `cast` inside logical expressions. Due to the way assertions are generated, as `assert` statements before the cast expression, the interpreter will eagerly evaluate them even if there value will be short-circuited by a logical operator. Another issue addressed in that section is the lack of runtime type checking of object members (properties and methods).
+There are a few known limitations and unwanted behaviors in the current version of Midas. The first, which has already been discussed in @sec:gen-assertions, concerns `cast` inside logical expressions. Due to the way assertions are generated, as `assert` statements before the cast expression, the interpreter will eagerly evaluate them even if their value will be short-circuited by a logical operator. Another issue addressed in that section is the lack of runtime type checking of object members (properties and methods).
 
 The way method resolution is implemented also makes the behavior of operators slightly differ from what the interpreter will do at runtime. For example, reverse operators (e.g. `__radd__`) are not looked up by Midas. This makes some operations invalid for Midas, such as `1 + 1.0`, while `1.0 + 1` is correctly type checked.
 
@@ -37,7 +37,7 @@ One last important issue with Midas as it is, which would require some work to f
 Some Python features are only partially supported or have been deliberately left out of the scope. Nevertheless, a few could be implemented without developing major new infrastructure.
 One example of such a feature are argument sinks, allowing variadic function definitions.
 
-There also a few builtin types and function which are missing from Midas' preamble. This includes the `Iterable` or `Sequence` types, currently replaced with `list` where needed. A number of builtin list-related functions also return some ad-hoc objects, like `range`, `filter`, `map` or `zip`.
+There are also a few builtin types and function which are missing from Midas' preamble. This includes the `Iterable` or `Sequence` types, currently replaced with `list` where needed. A number of builtin list-related functions also return some ad-hoc objects, like `range`, `filter`, `map` or `zip`.
 
 Several syntax elements could also be added relatively easily, such as `while` loops, `break` and `continue` statements, lambdas, `else` clauses on `for` loops and decorators.
 
@@ -53,7 +53,7 @@ Finally, the following are some ideas for extension of Midas, including new feat
 
 From a practical point of view, fully handling `import` statements would allow using Midas in more complex multi-file projects. This may allow distributing type definitions for packages too, similar to stubs.
 
-Similar to how dataframes are handled, our type system could also handle structure such as `numpy` arrays, which are extremely common in data science in particular.
+Akin to how dataframes are handled, our type system could also support structures such as `numpy` arrays, which are extremely common in data science in particular.
 
 Regarding constraint types, the current system could be improved by introducing a constraint solver capable of statically evaluating their domain and even allow subtyping rules such as $(x < 10) <: (x < 100)$.
 As mentioned in @sec:pipeline-type-checking, this could also lead to powerful type checking of aggregation methods by deriving domain constraints from the aggregation methods themselves. For example, the `mean` of positive numbers less than or equal to 100 is also a positive number less than or equal to 100.

report/pages/résumé.typ

@@ -11,9 +11,9 @@ En Python, la philosophie de _duck typing_ est souvent source d'erreurs, en part
 Midas est un nouveau système de types construit sur Python qui vise à offrir une vérification statique stricte et des assertions à l'exécution pour garantir l'intégrité des données.
 Midas inclut son propre langage de définition de types pour tous besoins spécifiques à un domaine.
 Il fournit également une vérification étendue des schémas et opérations sur les DataFrames Pandas, comme les méthodes d'agrégation.
-Les expression de casting sont vérifiée statiquement sur les valeurs littérales ou génèrent des assertions à l'exécution qui vérifient la conformité si elle ne peut pas être jugée à la compilation.
-L'entièreté du système est construit de zéro, à l'exception du parser pour le langage de définition qui est adapté d'un autre projet.
-Le système de type est dans un premier temps abordé d'un point de vu théorique, en puisant dans #acrfull("TaPL").
+Les expressions de casting sont vérifiées statiquement sur les valeurs littérales ou génèrent des assertions à l'exécution qui vérifient la conformité si elle ne peut pas être jugée à la compilation.
+L'ensemble du système est construit de zéro, à l'exception du parser pour le langage de définition qui est adapté d'un autre projet.
+Le système de types est dans un premier temps abordé d'un point de vu théorique, en puisant dans #acrfull("TaPL").
 L'implémentation est ensuite développée étape par étape, composant par composant.
 
 /*