fix(report): title case in headings

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/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.
 
@@ -100,7 +100,7 @@ Some syntaxes are simplified or omitted from @tab:python-syntax-rules for the sa
 
 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.
 
@@ -126,7 +126,7 @@ The last kind of statement provides users with a way to define named constraint
 
 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.
 
@@ -228,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/04_implementation/03_registry.typ

@@ -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
@@ -73,7 +73,7 @@ The `define_*` and `lookup_*`/`get_*` methods are quite straightforward, inserti
 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.
 
@@ -129,7 +129,7 @@ A second check in @fig:define_member:17 avoids redefining a member which is not
 
 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`).
 
@@ -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

@@ -18,7 +18,7 @@ Processing a Midas definitions file is done in 3 steps:
 
 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.
 
@@ -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.
 
@@ -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.
 

report/chapters/04_implementation/05_python_checking.typ

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

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,7 +59,7 @@ 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 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.
@@ -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`).