71 lines
7.0 KiB
Typst
71 lines
7.0 KiB
Typst
#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 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.
|
|
|
|
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 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.
|
|
|
|
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 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.
|
|
|
|
/*
|
|
- 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.
|
|
|
|
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.
|
|
/*
|
|
- 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.
|