feat(report): write conclusion

report/chapters/01_introduction.typ

@@ -29,7 +29,7 @@ As explained above, Python is a very flexible language, sometimes too flexible.
 
 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 for user 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 motivation for the famous Python library Pydantic, allowing users to define data structures that can validate inputs when instantiated.
 
 == Objectives
 

report/chapters/04_implementation/04_midas_language.typ

@@ -150,7 +150,7 @@ The basic members and methods referenced in implementations of this section are
 
 === 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 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.
+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.
 
 As an example, visiting a `m.NamedType` node simply looks up the name in the registry to retrieve the definition for that type. If it cannot be found, an error is reported to the user and `UnknownType` is returned. This is the standard behavior we will implement whenever the type checker cannot make a definite judgement about something. As you may notice in @fig:midas-visit_named_type, the implementation checks `self._current_name` to detect cyclic references. In @fig:midas-visit_named_type:4, `self.get_type` is used instead of directly calling the registry's method to handle type variables, as explained in @sec:midas-type-stmt.
 

report/chapters/04_implementation/05_python_checking.typ

@@ -394,7 +394,7 @@ Some other simple cases mentioned above can be handled with recursion. Calls to
 
 For `OverloadedFunction`, we must first resolve which overload the calls should use. We defer this process to a `_match_overload` method which we will build now.
 
-=== Matching Overload
+=== Matching Overload <sec:python-call-overload>
 
 This method receives the list of overloads and all call arguments. Its goal is to:
 1. identify which overload is compatible
@@ -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
+=== 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/04_implementation/06_generation.typ

@@ -27,7 +27,7 @@ In the end, an `ast.Module` is produced and unparsed into raw Python code. The f
 
 == Assertions <sec:gen-assertions>
 
-`Generator` also needs to produce assertions for each `cast` expression, as described in @sec:gen-assertions. Such expressions may appear anywhere in the program, including in other expressions. Because Python assertions are statements, we cannot simply insert them in the surrounding expression. Instead, the approach we implement is to define an alias variable for the expression, before the statement where it appears, add the `assert` statement and insert back the alias where the expression is used.
+`Generator` also needs to produce assertions for each `cast` expression. Such expressions may appear anywhere in the program, including in other expressions. Because Python assertions are statements, we cannot simply insert them in the surrounding expression. Instead, the approach we implement is to define an alias variable for the expression, before the statement where it appears, add the `assert` statement and insert back the alias where the expression is used.
 In practice, this looks like @fig:example-assert-alias.
 
 #figure(

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
+== 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
+=== 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
+=== 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.
 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
+== 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

@@ -1,4 +1,68 @@
 #import "../requirements.typ": isc-hei-bthesis
 #import isc-hei-bthesis: todo
+#import "../utils.typ": fn-link
+#import "@preview/acrostiche:0.7.0": acr
 
 = 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.
+
+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.
+
+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.
+
+== Future Work <sec:future-work>
+
+Although many features have been implemented and integrated into Midas, there is still a lot of potential to improve, complete and extend it.
+A non-exhaustive list of such opportunities and ideas has been compiled and organized hereafter into three categories.
+
+=== 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).
+
+In @sec:python-call-generic, we mentioned a `Unifier` class to help finding appropriate substitutions for type parameters of a generic function call. There is one case that is not yet handled however. This case concerns generic function calls with generic arguments. Chapter 22 of #acr("TaPL")@tapl on _Type Reconstruction_ provides some good leads to making `Unifier` more robust and complete.
+
+One last important issue with Midas as it is, which would require some work to fix, is the absence of a mechanism to handle references. Currently, the type checker expects that variable declared with a given type will remain structurally unchanged in the program's lifecycle. Unfortunately, this is simply not true with objects such as dataframes, which can have their schema modified somewhere, affecting other unrelated references. Some good first leads can be found in Chapter 13 of #acr("TaPL")@tapl on _References_.
+
+/*
+- unification with constraints (cf TAPL), e.g. when unifying with a generic type as the concrete
+- assertions bypass logic short-circuiting
+- check members
+*/
+
+=== Partial Features <sec:partial-features>
+
+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`.
+
+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.
+
+/*
+- argument sinks
+- more builtins: Iterable, map (type), range, filter, zip
+- more syntax: while loops, breaks / continue, decorators, lambdas, for-else
+*/
+
+=== Extensions <sec:extensions>
+
+Finally, the following are some ideas for extension of Midas, including new features that could be interesting to add following our motivations for creating Midas in the first place.
+
+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.
+
+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.
+/*
+- expected type
+- constraint solver
+- imports
+- numpy arrays
+- class definitions
+*/
+
+== Final Words <sec:final-words>
+
+On a personal level, this project brought me great satisfaction. Designing a custom language, implementing a parser and type checker from scratch were all highly gratifying and mobilized many skills and ideas. Being a math enthusiast, I also enjoyed discovering the more theoretical aspects of computer science, and reading the fundamental pillar that is #acr("TaPL") proved to be much more enjoyable than one might think.