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

feat(report): write Midas typer

Browse Source
This commit is contained in:
Louis Heredero
2026-07-18 19:06:04 +02:00
parent 49d5d321c8
commit ef2d74e889
4 changed files with 327 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
report/appendices/midas_typer_skeleton.typ Normal file
View File

@@ -0,0 +1,11 @@
#import "../requirements.typ": isc-hei-bthesis
#import isc-hei-bthesis: code
#figure(
code(raw(
read("../code/midas_typer_skeleton.py"),
lang: "python",
block: true
)),
caption: [Midas Typer Members]
) <fig:midas-typer-members>

2
report/bachelor_thesis.typ
View File

@@ -163,6 +163,8 @@ You can also change the order or the names of the sections, for instance, if you
#include "appendices/is_subtype.typ"
#include "appendices/midas_typer_skeleton.typ"
#pagebreak()
= Midas Language Definition <app:midas-syntax>

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

@@ -14,7 +14,7 @@ Processing a Midas definitions file is done in 3 steps:
Each of these steps map to a dedicated class, respectively `MidasLexer`, `MidasParser` and `MidasTyper`.
== Lexing and parsing
== Lexing and parsing <sec:midas-lexing-parsing>
The lexer and parser follow the structure presented by Nystrom@Nystrom2021 and implemented in #fn-link(<pebble-fn>, "https://git.kb28.ch/HEL/pebble")[pebble]@Pebble.
@@ -136,7 +136,231 @@ These tokens are then passed through the parser which builds an #acr("AST") show
After passing through `MidasParser`, we thus obtain a stable and explicit structure that can be given to `MidasTyper` and interpreted (as far as a definition language can be interpreted).
== Processing statements
== Processing statements <sec:midas-interpretation>
Each statement is processed in order. In the following sections we will get in more details for each kind of statements, and look at how we can implement their effects on the types registry.
The complete implementation of `MidasTyper` is available in the project's repository in #code-ref(<midas-typer>, "midas/checker/midas.py").
The basic members and methods referenced in implementations of this section are listed in @fig:midas-typer-members.
=== Building types <sec:midas-building-types>
Before we can register a new type or an alias, we must be able to convert an #acr("AST") representation of a type into our internal type representation structures. For this we leverage the visitor pattern by implementing the visitor class of `Type` #acr("AST") nodes, as generated in @sec:midas-lexing-parsing. We thus make `MidasTyper` extend `m.Type.Visitor[Type]`#footnote[To avoid confusion between Midas and Python AST nodes, their namespaces are imported as `m` and `p` respectively. A standalone reference to `Type` relates to the union of internal type representations mentioned in @sec:impl-types.]<fn:types-ref>, indicating that it must handle visiting any `m.Type` node and return a `Type` object.
As an example, visiting a `m.NamedType` node simply looks up the name in the registry to retrieve the definition for that type. If it cannot be found, an error is reported to the user and `UnknownType` is returned. This is the standard behavior we will implement whenever the type checker cannot make a definite judgement about something. As you may notice in @fig:midas-visit_named_type, the implementation checks `self._current_name` to detect cyclic references. In @fig:midas-visit_named_type:4, `self.get_type` is used instead of directly calling the registry's method to handle type variables, as explained in @sec:midas-type-stmt.
#figure(
```python
def visit_named_type(self, type: m.NamedType) -> Type:
name: str = type.name.lexeme
try:
return self.get_type(name)
except NameError:
msg: str = f"Undefined type {name}"
if self._current_name == name:
msg += ". Recursive types are not supported, use an extend block"
self.reporter.error(type.name.get_location(), msg)
return UnknownType()
```,
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.
#figure(
```python
def visit_generic_type(self, type: m.GenericType) -> Type:
match type.type:
case m.NamedType(name=Token(lexeme="Column")):
if len(type.args) != 1:
self.reporter.error(
type.location,
f"Column requires 1 type argument, {len(type.args)} provided",
)
return ColumnType(type=UnknownType())
return ColumnType(type=type.args[0].accept(self))
type_: Type = type.type.accept(self)
args: list[Type] = [arg.accept(self) for arg in type.args]
try:
return self.types.apply_generic(type_, args)
except Exception as e:
self.reporter.error(type.location, f"Cannot apply generic type: {e}")
return UnknownType()
```,
caption: [Midas Typer: implementation of `visit_generic_type`]
) <fig:midas-visit_generic_type>
Constraint types also need some special handling because they include an `m.Expr` node for the constraint expression. This expression is type checked, like Python code will, ensuring that operations are coherent and that the resulting type is a boolean. For more information, please refer to @sec:midas-checking-expr.
#figure(
```python
def visit_constraint_type(self, type: m.ConstraintType) -> Type:
base_type: Type = type.type.accept(self)
self._predicate_params["_"] = base_type
constraint_type: Type = self.type_of(type.constraint)
self._predicate_params = {}
if not self.types.is_subtype(constraint_type, self._bool):
self.reporter.error(
type.constraint.location,
f"Constraint must evaluate to a boolean, got {constraint_type}",
)
return ConstraintType(
type=base_type,
constraint=type.constraint,
)
```,
caption: [Midas Typer: implementation of `visit_constraint_type`]
) <fig:midas-visit_constraint_type>
As you can see in the implementation above, in @fig:midas-visit_constraint_type, we insert the base type as `"_"` in an internal `_predicate_params` dictionary. This will be used later when type checking expression (@sec:midas-checking-expr) to retrieve the "current" type when using a `m.WildcardExpr`.
Processing functions and dataframe types is naturally implemented by processing their internal types (e.g. parameters, columns) and building the corresponding internal representations.
=== 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:
+ 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.)
If all three lookups fail, `UnknownType` is returned and an error is reported.
=== Alias statement <sec:midas-alias-stmt>
Now that we can build types we must implement a way to register them for future reference.
The first and simplest statement is the alias statement (`m.AliasStmt`). Its effect is to bind the given name to the type defined on the right-hand side. The implementation is quite straightforward, as demonstrated in @fig:midas-visit_alias_stmt. Do note that `self._current_name` is set before processing the `m.Type` node, and cleared afterwards, so that cyclic references can be caught. The exception raised by the registry is also caught and reported through an error diagnostic to continue processing remaining statements.
#figure(
```python
def visit_alias_stmt(self, stmt: m.AliasStmt) -> None:
name: str = stmt.name.lexeme
self._current_name = name
type: Type = stmt.type.accept(self)
try:
self.types.define_type(name, type)
except ValueError:
self.reporter.error(stmt.location, f"Type {name} already defined")
self._current_name = None
```,
caption: [Midas Typer: implementation of `visit_alias_stmt`]
) <fig:midas-visit_alias_stmt>
=== Type statement <sec:midas-type-stmt>
Type statements work similarly to alias statements, though they wrap the defined type in a `DerivedType` or `GenericType` depending on whether there are parameters.
Additionally, if parameters are given, they are processed and transformed into `TypeVar` instances, and registered in an internal `_local_variables` dictionary. This internal registry is used by `TypesRegistry.get_type` to resolve references to type variables inside generic types and `extend` statements.
#figure(
```python
def visit_type_stmt(self, stmt: m.TypeStmt) -> None:
name: str = stmt.name.lexeme
self._current_name = name
params: list[TypeVar] = self._resolve_type_params(stmt.params)
type: Type = stmt.type.accept(self)
if len(params) != 0:
type = GenericType(name=name, params=params, body=type)
else:
type = DerivedType(name=name, type=type)
try:
self.types.define_type(name, type)
except ValueError:
self.reporter.error(stmt.location, f"Type {name} already defined")
self._local_variables.clear()
self._current_name = None
def _resolve_type_params(self, params: list[m.TypeParam]):
vars: list[TypeVar] = []
for param in params:
name: str = param.name.lexeme
bound: Optional[Type] = None
if param.bound is not None:
bound = param.bound.accept(self)
var = TypeVar(name=name, bound=bound)
self._local_variables[name] = var
vars.append(var)
return vars
```,
caption: [Midas Typer: implementation of `visit_type_stmt`]
) <fig:midas-visit_type_stmt>
=== 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.
#figure(
```python
def visit_predicate_stmt(self, stmt: m.PredicateStmt) -> None:
name: str = stmt.name.lexeme
for spec in stmt.params:
for param in spec.mixed:
assert param.name is not None
self._predicate_params[param.name.lexeme] = param.type.accept(self)
type: Type = self.type_of(stmt.body)
params: list[ParamSpec] = [self._visit_param_spec(spec) for spec in stmt.params]
if not self._is_valid_predicate(type):
self.reporter.error(
stmt.body.location,
f"Predicate function body must evaluate to a boolean, got {type}",
)
if len(params) != 0:
type = self._bool
for spec in reversed(params):
type = Function(
params=spec,
returns=type,
)
self._predicate_params = {}
try:
self.types.define_predicate(
name,
Predicate(
type=type,
body=stmt.body,
alias=len(params) == 0,
),
)
except ValueError:
self.reporter.error(stmt.location, f"Predicate {name} already defined")
def _is_valid_predicate(self, body: Type) -> bool:
match body:
case Function(returns=returns):
return self._is_valid_predicate(returns)
case _ if self.types.is_subtype(body, self._bool):
return True
case _:
return False
```,
caption: [Midas Typer: implementation of `visit_predicate_stmt`]
) <fig:midas-visit_predicate_stmt>
== Example
Continuing with our example from @fig:example-midas-ast, the type statement would register a new type named `Kelvin` with internal representation given in
#figure(
```python
DerivedType(
name='Kelvin',
type=ConstraintType(
type=BaseType(name='float'),
constraint=BinaryExpr(
left=WildcardExpr(
token=Token(type=TokenType.UNDERSCORE, lexeme='_', value=None)
),
operator=Token(type=TokenType.GREATER_EQUAL, lexeme='>=', value=None),
right=LiteralExpr(value=0)
)
)
)
```,
caption: [Midas Example: registered type#footnote[Location and position objects are omitted for readability]]
) <fig:example-midas-type>
/*
- Midas definition language

88
report/code/midas_typer_skeleton.py Normal file
View File

@@ -0,0 +1,88 @@
class MidasTyper(m.Stmt.Visitor[None], m.Expr.Visitor[Type], m.Type.Visitor[Type]):
logger: logging.Logger
reporter: FileReporter
types: TypesRegistry
dispatcher: CallDispatcher[m.Expr]
_local_variables: dict[str, TypeVar]
_predicate_params: dict[str, Type]
_current_name: Optional[str]
_preamble: Environment
def type_of(self, expr: m.Expr) -> Type:
"""Compute the type of the given expression
Args:
expr (m.Expr): the expression to type
Returns:
Type: the type of the expression
"""
type: Type = expr.accept(self)
return type
def get_type(self, name: str) -> Type:
"""Get a type from its name
Args:
name (str): the name of the type
Raises:
NameError: if the type is not defined
Returns:
Type: the type
"""
if name in self._local_variables:
return self._local_variables[name]
return self.types.get_type(name)
def get_variable(self, location: Location, name: str) -> Type:
"""Get the type of a variable
This function will first look into the current predicate's parameters if
we are in a predicate definition.
The the variable is looked up in the preamble (i.e. global environment)
Args:
location (Location): the location of the variable reference
name (str): the name of the variable
Returns:
Type: the type of the variable
"""
if name in self._predicate_params:
return self._predicate_params[name]
predicate: Optional[Predicate] = self.types.lookup_predicate(name)
if predicate is not None:
return predicate.type
global_: Optional[Type] = self._preamble.get(name)
if global_ is not None:
return global_
self.reporter.error(location, f"Unknown variable '{name}'")
return UnknownType()
def resolve(self, stmts: list[m.Stmt]):
"""Process a sequence of statements
Args:
stmts (list[m.Stmt]): the statements
"""
for stmt in stmts:
stmt.accept(self)
manager: VarianceManager = VarianceManager(self.types)
manager.infer_all()
def assert_bool(self, expr: m.Expr):
"""Check that the given expression is a subtype of `bool` or report an error
Args:
expr (m.Expr): the expression to check
"""
type: Type = self.type_of(expr)
if not self.types.is_subtype(type, self._bool):
self.reporter.error(expr.location, f"Must be a boolean but is {type}")