fix(report): typos
This commit is contained in:
@@ -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
|
||||
|
||||
|
||||
@@ -8,12 +8,12 @@
|
||||
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.
|
||||
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.
|
||||
|
||||
@@ -98,7 +98,7 @@ 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>
|
||||
|
||||
@@ -120,9 +120,9 @@ 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.
|
||||
|
||||
@@ -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.
|
||||
|
||||
|
||||
@@ -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_]),
|
||||
|
||||
@@ -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(
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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.
|
||||
|
||||
@@ -70,8 +70,8 @@ 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`
|
||||
|
||||
@@ -127,7 +127,7 @@ 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`
|
||||
|
||||
@@ -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.
|
||||
|
||||
@@ -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>
|
||||
|
||||
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
|
||||
@@ -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
|
||||
@@ -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.
|
||||
|
||||
|
||||
@@ -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.
|
||||
|
||||
@@ -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.
|
||||
|
||||
@@ -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
|
||||
@@ -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),
|
||||
@@ -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.
|
||||
|
||||
@@ -571,10 +571,10 @@ We will explore in this section how we can not only provide type-checking for fr
|
||||
|
||||
=== 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,7 +632,7 @@ 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"$].
|
||||
|
||||
@@ -645,7 +645,7 @@ All implementations of the classes discussed in this section are available in th
|
||||
|
||||
== 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.
|
||||
|
||||
@@ -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.
|
||||
|
||||
@@ -61,7 +61,7 @@ Finally, we can concisely define frame schemas that will become useful when mani
|
||||
|
||||
=== 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),
|
||||
|
||||
@@ -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 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.
|
||||
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.
|
||||
|
||||
@@ -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.
|
||||
|
||||
/*
|
||||
|
||||
Reference in New Issue
Block a user