HEL/TB-Docs
1
0
Fork 0
Code Issues Pull Requests Releases Activity

feat(report): work on some python expressions

Browse Source
This commit is contained in:
Louis Heredero
2026-07-19 19:14:22 +02:00
parent c866a6a1d9
commit d4e603c5b1
4 changed files with 71 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
report/chapters/03_theory.typ
View File

@@ -139,7 +139,7 @@ First and foremost, we can define elementary typing rules for all literal values
supplement: [Table],
) <tab:typing-literals>
Other constructs, although not constants, directly map to builtin types. These include literal lists, tuples and dictionaries. Each of these has a corresponding `list[T]`, `tuple` and `dict[K, V]` type. We will not define formal rules in this section regarding these elements, but a more in depth explanation will be given in the implementation of the type checker, in @sec:impl-python. #todo[replace ref]
Other constructs, although not constants, directly map to builtin types. These include literal lists, tuples and dictionaries. Each of these has a corresponding `list[T]`, `tuple` and `dict[K, V]` type. We will not define formal rules in this section regarding these elements, but a more in depth explanation will be given in the implementation of the type checker, in @sec:python-check-literals.
=== Expressions <sec:typing-expressions>
@@ -181,7 +181,7 @@ Finally, expressions can be used in statements, which are special constructs tha
You may be familiar with the walrus operator `:=` which is often used in `if` statements to simultaneously declare a variable and use it as an expression. It it thus a mix between a simple expression, which may be used everywhere, and a statement, with the side-effect of declaring a variable.
]
#smallcaps[T-Def] is a gross simplification of how functions can be defined. It does not cover multiple parameters, positional-only and keyword-only parameters, complex bodies with multiple and implicit returns, etc. Again, for the sake of simplicity and readability, we will not define a complete rule to handle all forms and features, but the implementation will go into more details in @sec:impl-python. #todo[replace ref]
#smallcaps[T-Def] is a gross simplification of how functions can be defined. It does not cover multiple parameters, positional-only and keyword-only parameters, complex bodies with multiple and implicit returns, etc. Again, for the sake of simplicity and readability, we will not define a complete rule to handle all forms and features, but the implementation will go into more details in @sec:python-functions.
=== Subtyping <sec:typing-subtyping>
@@ -208,7 +208,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:impl-python #todo[replace ref].
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.
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.

4
report/chapters/04_implementation/02_types.typ
View File

@@ -48,7 +48,7 @@ A similar approach is used for constraint types, by embedding the base type and
== Generic Types
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:impl-midas #todo[replace ref].
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.
@@ -148,4 +148,4 @@ This class holds three properties of predicates:
- `type`: the function signature of the predicate.\
For example, ```midas predicate less_than(max: float)(v: float) = v < max``` has the signature ```midas fn(max: float) -> fn(v: float) -> bool```
- `body`: the raw predicate expression. This will be used to generate equivalent Python code and perform static checks against literal values
- `alias`: a flag indicating whether a predicate is a simple alias of another, used for example with partially applied predicates (see @sec:impl-midas #todo[replace ref])
- `alias`: a flag indicating whether a predicate is a simple alias of another, used for example with partially applied predicates (see @sec:midas-predicate-stmt)

6
report/chapters/04_implementation/04_midas_language.typ
View File

@@ -223,8 +223,8 @@ Processing functions and dataframe types is naturally implemented by processing
=== Type checking expressions <sec:midas-checking-expr>
The process of type checking constraint expressions (`m.Expr`) is nearly identical to type checking a Python expression. Thus, the implementation is quite similar. This will be covered in the section concerning `PythonTyper`, i.e. @sec:impl-python #todo[replace ref].
For now, we only look at `visit_variable_expr` and `visit_wildcard_expr` which call `get_variable` to return the type of the variable referenced. This method is detailed in @fig:midas-typer-members and, in essence does the following:
The process of type checking constraint expressions (`m.Expr`) is nearly identical to type checking a Python expression. Thus, the implementation is quite similar. This will be covered in the section concerning `PythonTyper`, i.e. @sec:python-check-expr.
For now, we only look at `visit_variable_expr` and `visit_wildcard_expr` which call `get_variable` to return the type of the referenced variable. This method is detailed in @fig:midas-typer-members and in essence does the following:
+ Look up the variable in the list of predicate parameters (including `_`)
+ Look up any predicate with the given name
+ Look up in the global environment or preamble for a builtin with the given name (e.g. `float`, `len`, etc.)
@@ -291,7 +291,7 @@ Additionally, if parameters are given, they are processed and transformed into `
=== Predicate statement <sec:midas-predicate-stmt>
When processing a predicate definition, we first need gather all parameters and register them internally in `self._predicate_params`. Then we type check the predicate body, i.e. a constraint expression (`m.Expr`). After this we process all parameter specifications using the same method as for function types. Before defining the predicate, we also check that the body's type is valid, i.e. a subtype of `bool` or a function which returns a valid predicate (in case of a partially applied predicate). Lastly, we build a complete function signature for the predicate, combining curried parameter specifications into functions returning functions, and insert it in the registry. This whole procedure is implemented as shown in @fig:midas-visit_predicate_stmt.
When processing a predicate definition, we first need to gather all parameters and register them internally in `self._predicate_params`. Then we type check the predicate body, i.e. a constraint expression (`m.Expr`). After this we process all parameter specifications using the same method as for function types. Before defining the predicate, we also check that the body's type is valid, i.e. a subtype of `bool` or a function which returns a valid predicate (in case of a partially applied predicate). Lastly, we build a complete function signature for the predicate, combining curried parameter specifications into functions returning functions, and insert it in the registry. If the predicate definition does not include any parameter specification, we mark it as an alias. This whole procedure is implemented as shown in @fig:midas-visit_predicate_stmt.
#figure(
```python

65
report/chapters/04_implementation/05_python_checking.typ
View File

@@ -246,7 +246,7 @@ In the case of functions, this means that the user should be allowed to omit the
#[
+ Type check the function's body, collecting return types in the environment
+ If no return statement appears in the body, default to `UnitType`
+ Try and find a #acr("LUB") of all return types, only in this list of types#footnote[We check whether one of the types in the list is a supertype of all the others]
+ Try and find a #acr("LUB") of all return types, only in this list of types#footnote[We check whether one of the types in the list is a supertype of all the others ($exists t_r in TT : forall t in TT, t <: t_r$)]
+ Unique return supertype?
- *Yes*: use it as the inferred return type
- *No*: report an error and use `UnknownType` as the inferred return type
@@ -267,7 +267,68 @@ In the case of functions, this means that the user should be allowed to omit the
The complete implementation of `PythonTyper.visit_function` is listed in @fig:python-visit_function.
== Type Checking Expressions <sec:python-check-expr>
#todo[]
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.
=== Literals <sec:python-check-literals>
Applying typing rules for literals (@tab:typing-literals) is only a matter of matching each value type to the corresponding builtin type representation, as shown in @fig:python-visit_literal_expr.
#figure(
```python
def visit_literal_expr(self, expr: p.LiteralExpr) -> Type:
match expr.value:
case bool(): return self.types.get_type("bool")
case int(): return self.types.get_type("int")
case float(): return self.types.get_type("float")
case str(): return self.types.get_type("str")
case None: return self.types.get_type("None")
case _:
self.reporter.warning(expr.location, f"Unknown literal {expr}")
return UnknownType()
```,
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.
#figure(
```python
def visit_list_expr(self, expr: p.ListExpr) -> Type:
list_type: Type = self.types.get_type("list")
item_types: list[Type] = [self.type_of(item) for item in expr.items]
item_types = self.types.reduce_types(item_types)
if len(item_types) == 0:
return list_type
if len(item_types) == 1:
item_type: Type = item_types[0]
return self.types.apply_generic(list_type, [item_type])
self.reporter.warning(
expr.location,
f"Heterogeneous list items: [{', '.join(map(str, item_types))}]",
)
return self.types.apply_generic(list_type, [UnknownType()])
```,
caption: [Python Typer: implementation of `visit_list_expr`]
) <fig:python-visit_list_expr>
Literal dictionaries are handled in the same manner, finding a supertype for keys and for values.
=== Operations
In Python, builtin operators are implemented through _dunder-methods_, i.e. methods on the operands. To the eyes of the type checker, an operation is thus equivalent to a function call. We can implement this idea by following these steps:
+ Get the dunder-method name corresponding to the operator
+ Type-check all operands (two for binary operators, one for unary operators)
+ Lookup the method on the left operand#footnote[Reverse operations (e.g. `__radd__`) have not been implemented in Midas yet]
+ Type check a call to the method with the given operand(s)
Step 1 is a simple lookup in a dictionary.\
Step 2 is a recursive call to type check the operand expressions.\
Step 3 calls `TypesRegistry.lookup_member`.\
Step 4 is delegated to a common `call_method` function, also used for call expressions (see @sec:python-check-calls).
Similarly, subscripts are de-sugared into calls to `__getitem__`.
== Type Checking Calls <sec:python-check-calls>
#todo[]