fix(report): consistent spelling

report/chapters/02_state_of_the_art.typ

@@ -7,7 +7,7 @@
 
 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.
+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.\

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/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").
 
@@ -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)
 
@@ -562,10 +562,10 @@ 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)
 
@@ -638,14 +638,14 @@ Column aggregation does have a pretty stable and predictable output. Taking the
 
 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 (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.
+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/05_results_discussion.typ

@@ -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.
 

report/chapters/06_conclusion.typ

@@ -5,7 +5,7 @@
 
 = 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 functions or accessing object attributes.