feat(report): complete python type checking

report/acronyms.typ

@@ -5,6 +5,7 @@
   "LSP": (link("https://en.wikipedia.org/wiki/Liskov_substitution_principle")[Liskov substitution principle],),
   "AST": ([Abstract Syntax Tree],),
   "LUB": ([Least Upper Bound],),
+  "CLI": ([Command-Line Interface],),
 )
 
 #init-acronyms(acronyms)

report/chapters/03_theory.typ

@@ -154,6 +154,8 @@ Apart from literals, developers also need some building blocks to express their
 
 #smallcaps[T-Var] simply states that a variable can be typed iff it is in the context.
 
+#smallcaps[T-Cast] is the equivalent of Pierce's ascription rule #smallcaps[T-Ascribe] (see chapter 11 of #acr("TaPL")@tapl), allowing users to cast any expression to a given type. Should the premise not be verifiable at compile-time, a runtime assertions will be generated.
+
 #smallcaps[T-Call] is a simplified rule of the concrete behavior. Taking into account all call forms with positional and keyword arguments is a rather tedious process which is left as an exercise to the reader.
 
 #smallcaps[T-Tern] is worth a few more words too. Typing rules used by Midas are, by design, stricter than what Python allows. In this case, because we have chosen not to include union types, an expression can only have at most one type, thus the branches must belong to a common type. The specific types of each branch may differ thanks to #smallcaps[T-Sub], defined in @tab:typing-subtyping-base. Additionally, the test expression must be of type $"bool"$, whereas Python can evaluate any object to a boolean.

report/chapters/03_theory/typing.typ

@@ -60,6 +60,12 @@
     $Gamma tack "x": "T"$,
     ```py x```,
   ),
+  rule(
+    "T-Cast",
+    $Gamma tack "t": "T"$,
+    $Gamma tack #syntax[cast] ("T", "t"): "T"$,
+    ```py cast(float, x)```
+  ),
   rule(
     "T-Call",
     $Gamma tack f: "T"_1 -> "T"_2$,

report/chapters/04_implementation/02_types.typ

@@ -9,7 +9,7 @@ Before we can parse type definitions or type check Python code, we need to defin
 
 In our type system, we will indeed have different kinds of types with different properties. All types described in this section are grouped under a union type named `Type` for easier references in annotations. Additionally, we will later need to define some basic functions to manipulate types, for example to substitute parameters in a generic type. These functions will be introduced where needed in later sections. The source code for internal type representations and these basic functions is available in the repository in #code-ref(<types>, "midas/checker/types.py").
 
-== Base Types
+== 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.
@@ -27,7 +27,7 @@ For the special `tuple` type, we can define a more specific class which can hold
   caption: [Type kinds: base types]
 ) <fig:types-base-types>
 
-== Derived Types
+== Derived Types <sec:types-derived-types>
 
 When defining subtypes in Midas, we will need to store that link in the registry. There are multiple approaches to subtyping, which can either be nominal or structural. In the case of Midas, we will generally stick to nominal subtyping, i.e. subtypes are explicitly defined, with some exceptions like constraint types and function types, as described in @sec:typing-subtyping.
 
@@ -46,7 +46,7 @@ A similar approach is used for constraint types, by embedding the base type and
   caption: [Type kinds: derived types]
 ) <fig:types-derived-types>
 
-== Generic Types
+== Generic Types <sec:types-generics>
 
 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.
@@ -76,7 +76,7 @@ These types are implemented by the classes in @fig:types-generics.
   caption: [Type kinds: generic types]
 ) <fig:types-generics>
 
-== Function Types
+== Function Types <sec:types-functions>
 
 As noted in the theory chapter (@chap:theory), functions in Python are complex and highly flexible.
 A function type thus have a parameter specification and a return type. That parameter specification contains three kinds of parameters: positional-only (`pos`), keyword-only (`kw`) and mixed (`mixed`).
@@ -107,7 +107,7 @@ Finally, we will also define a structure to hold multiple signature of an overlo
   caption: [Type kinds: function types]
 ) <fig:types-functions>
 
-== Dataframe types
+== Dataframe types <sec:types-dataframes>
 
 Because Midas has been designed with data scientists in mind, it will also try and type check some common dataframe operations. To do so, we want the user to be able to define dataframe schemas and use their columns. We thus define `ColumnType` and `DataFrameType` in @fig:types-dataframes, which can be thought of as more abstract representations of Pandas' `Series` and `DataFrame`. Additionally, we define special objects to handle group-by entities which are intermediary values used when computing aggregations. These group-by types are necessary to distinguish them from the base dataframe or column because they provide different methods.
 
@@ -130,7 +130,7 @@ Because Midas has been designed with data scientists in mind, it will also try a
   caption: [Type kinds: dataframe types]
 ) <fig:types-dataframes>
 
-== Predicates
+== Predicates <sec:types-predicate>
 
 Although not types, predicates will also be represented by similar dataclasses in the types registry, as defined in @fig:types-predicate.
 

report/chapters/04_implementation/05_python_checking.typ

@@ -99,7 +99,11 @@ More generally, if all sub-branches assign to a variable, we can consider it def
 
 == Environments <sec:python-env>
 
-#todo[]
+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.
+
+The source code for `Environment` and `Preamble` is available in the repository in #code-ref(<env>, "midas/checker/environment.py") and #code-ref(<preamble>, "midas/checker/preamble.py") respectively.
 
 == Type Checking Statements <sec:python-check-stmt>
 
@@ -481,14 +485,182 @@ Using this class, we can complete `get_result` with the last case handling calls
 ) <fig:dispatcher-match-generic>
 
 == Casts and Static Evaluation <sec:python-check-casts>
-#todo[]
+
+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`.
+
+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.
+
+#figure(
+  ```python
+  def visit_cast_expr(self, expr: p.CastExpr) -> Type:
+      subject_type: Type = self.type_of(expr.expr)
+      target_type: Type = self.resolve_type_expr(expr.type)
+      is_lit, lit_value = self._get_literal(expr.expr)
+      if is_lit:
+          evaluated: bool = self._evaluate_cast_statically(
+              expr, subject_type, target_type, lit_value
+          )
+          if evaluated:
+              self.evaluated_casts.append(expr)
+      return target_type
+  ```,
+  caption: [Python Typer: implementation of `visit_cast_expr`]
+) <fig:python-visit_cast_expr>
+
+=== 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.
+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.
+
+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").
+
+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.
+
+#figure(
+  ```midas
+  predicate in_range(min: float, max: float)(v: float) = min <= v & v <= max
+  type Ratio = float where in_range(0.0, 1.0)(_)
+  ```,
+  caption: [Example of curried predicate application]
+) <fig:example-curried-application>
+
+In practice, we keep track of a scope dictionary containing all defined variables (parameters). When the first call is evaluated, we insert `min = 0.0` and `max = 1.0` in the scope and build a `PartialPredicate` object. This object contains the inner predicate function signature (`fn(float) -> bool`), the predicate's body (`min <= v & v <= max`) and the scope dictionary. The second call receives this `PartialPredicate` as the callee, inserts `_ = <the literal value>` in the scope and evaluates the predicate's body. This whole process is detailed in @fig:static-predicate-eval.
+
+#figure(
+  ```python
+  def _evaluate_predicate(
+      self,
+      location: Location,
+      predicate: Predicate,
+      args: list[Any],
+      kwargs: dict[str, Any],
+  ) -> Any:
+      res: Any = None
+      if isinstance(predicate, PartialPredicate):
+          self.scopes.append(predicate.scope)
+      else:
+          self.scopes.append({})
+      match predicate.type:
+          case Function(returns=Function() as inner):
+              self._map_args(location, predicate.type, args, kwargs)
+              res = PartialPredicate(
+                  type=inner,
+                  body=predicate.body,
+                  alias=False,
+                  scope=self.scopes[-1],
+              )
+          case Function():
+              self._map_args(location, predicate.type, args, kwargs)
+              res = self.evaluate(predicate.body)
+          case _:
+              raise NotImplementedError
+      self.scopes.pop()
+      return res
+  ```,
+  caption: [Static predicate evaluation]
+) <fig:static-predicate-eval>
 
 == Frames and Columns <sec:python-df-cols>
-#todo[]
+
+There is still one big part of the type checker that we have not covered: dataframes and columns. Properly type checking dataframe operations is a never-ending rabbit hole. Libraries like `pandas` or `polars` provide a enormous amount of features, as methods and syntax sugars. They also have highly polymorphic functions, accepting operations with all kinds of values, such as multiplying a dataframe by a scalar, a list, a column or even another dataframe. The results of these operations may vary quite a lot depending on the operands, or sometimes on the parameters passed to some functions. As discussed in @chap:state-of-the-art, some libraries do try and make developers' lives a little better by providing some static type-checking like #fn-link(<strictly-typed-pandas>, "https://strictly-typed-pandas.readthedocs.io")[_Strictly Typed Pandas_], or runtime schema verification like #fn-link(<pandera>, "https://pandera.readthedocs.io")[_Pandera_].
+
+Midas stands in between by providing some static type-checking for dataframe schemas and operations as well as generating runtime checks when a value is cast to such a type.
+We will explore in this section how we can not only provide type-checking for frame columns, for either accessing or assigning to them, but also handle some method calls with best effort inference of the resulting type.
+
+=== 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.
+
+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`.
+
+=== Method Registries <sec:python-df-methods>
+
+We will consider two kinds of methods:
+- element-wise binary operations
+- aggregation methods
+
+The first includes all arithmetic operations such as addition between two dataframes or columns. Adding two dataframes consists of pairing up matching columns and adding them together. Adding two columns consists of adding each corresponding items. In the example of @fig:example-df-add, we want to type check `__add__` on `df1` given `df2` as the second operand.
+
+#figure(
+  grid(
+    columns: (1fr, 1fr),
+    column-gutter: 1em,
+    ```midas
+    alias Frame1 = Frame[
+        a: float,
+        b: float
+    ]
+    alias Frame2 = Frame[
+        a: int,
+        b: str,
+        c: bool
+    ]
+    ```,
+    ```python
+    df1: Frame1
+    df2: Frame2
+
+    df3 = df1 + df2
+    ```,
+  ),
+  caption: [Example addition of dataframes]
+) <fig:example-df-add>
+
+Because it is an element-wise binary operation, we first match columns between both frame schemas:
+- `a: Column[float] + Column[int]`
+- `b: Column[float] + Column[str]`
+- `c: ? + Column[bool]`
+
+No `c` column is defined in `df1` which makes the resulting dataframe include an unknown column `c: Column[<Unknown>]`. For `a` and `b`, we then defer back to `CallDispatcher` for inferring the result of column addition.
+
+When adding two columns together, we proceed in a similar way by looking up the operation on the columns' inner types. Consequently, we must check that `float + int`, respectively `float + str`, are valid operations and use the result to form a new column. The former is valid in Python whereas the latter is not. This results in the new schema shown in @fig:example-df-add-result.
+
+#figure(
+  ```
+  df3: Frame[
+    a: float,
+    b: <Unknown>,
+    c: <Unknown>
+  ]
+  ```,
+  caption: [Dataframe addition resulting schema]
+) <fig:example-df-add-result>
+
+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.
+
+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"$].
+
+Some other aggregation methods have even simpler formulae, such as ```py median = lambda t: t```, but some may not be represented in this form, such as the `std` or `kurtosis` methods. These simply return a top type.
+
+One last important construct that Midas supports is the `groupby` method. This method allows partitioning a column or dataframe in groups, according to some criteria, and compute some aggregations on each one. Recall @sec:types-dataframes where we defined special type kinds `FrameGroupBy` and `ColumnGroupBy`. We now use them as results of `DataFrameType.groupby` and `ColumnType.groupby` respectively, and implement dedicated method registries for each one. Their methods only include aggregation methods. This time, we can properly implement them for dataframes, because type-checking an aggregation method on a `FrameGroupBy` is equivalent to type-checking the method on `ColumnGroupBy` instances of each column, combining the result in a new `DataFrameType`. The actual type-checking computation is thus deferred to the other registry for `ColumnGroupBy` methods.
+In turn this registry simply delegates to `ColumnMethodRegistry`.
+
+All implementations of the classes discussed in this section are available in the repository in #code-ref(<df-methods>, "midas/checker/frames/").
 
 == Output <sec:python-output>
-#todo[]
 
+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 #fn-link(<manual>, "docs/manual.pdf")[manual] which provides detailed explanation 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.
+
+We thus define a structure to hold the parsed #acr("AST"), all typing judgments made by the type checker, inline assertions and cast expressions which have already been statically evaluated. Indeed, cast expressions which were evaluated in @sec:python-evaluator do not need to generate runtime checks. This output structure is defined in @fig:typed-ast.
+
+#figure(
+  ```python
+  class TypedAST:
+      stmts: list[p.Stmt]
+      judgements: list[tuple[p.Expr, Type]]
+      evaluated_casts: list[p.CastExpr]
+      assertions: AssertionCollector
+  ```,
+  caption: [Python Typer: output `TypedAST` structure]
+) <fig:typed-ast>
 
 /*
 - Python type checking