feat(report): write section about variance inference

This commit is contained in:
HEL
2026-07-19 11:59:46 +02:00
parent 11420c690c
commit d55c5e325c
7 changed files with 221 additions and 5 deletions
+7 -5
View File
@@ -1,11 +1,13 @@
#import "../requirements.typ": isc-hei-bthesis
#import isc-hei-bthesis: code
#let midas-typer-members-code = raw(
read("../code/midas_typer_skeleton.py"),
lang: "python",
block: true
)
#figure(
code(raw(
read("../code/midas_typer_skeleton.py"),
lang: "python",
block: true
)),
code(midas-typer-members-code),
caption: [Midas Typer Members]
) <fig:midas-typer-members>
+29
View File
@@ -0,0 +1,29 @@
#import "../requirements.typ": isc-hei-bthesis
#import isc-hei-bthesis: code
#figure(
code(raw(
block: true,
lang: "python",
read("../code/variance_tracker.py")
)),
caption: [Implementation of variance `Tracker`]
) <fig:midas-variance-tracker>
#figure(
code(raw(
block: true,
lang: "python",
read("../code/variance_inferrer.py")
)),
caption: [Implementation of variance `VarianceInferrer`]
) <fig:midas-variance-inferrer>
#figure(
code(raw(
block: true,
lang: "python",
read("../code/variance_manager.py")
)),
caption: [Implementation of variance `VarianceManager`]
) <fig:midas-variance-manager>
+2
View File
@@ -165,6 +165,8 @@ You can also change the order or the names of the sections, for instance, if you
#include "appendices/midas_typer_skeleton.typ"
#include "appendices/variance.typ"
#pagebreak()
= Midas Language Definition <app:midas-syntax>
@@ -2,6 +2,8 @@
#import isc-hei-bthesis: todo
#import "../../utils.typ": fn-link, code-ref
#import "@preview/acrostiche:0.7.0": acr
#import "../../appendices/midas_typer_skeleton.typ": midas-typer-members-code
#import "@preview/codly:1.3.0": codly
= Midas Definition Processing <sec:impl-midas>
@@ -339,6 +341,10 @@ When processing a predicate definition, we first need gather all parameters and
caption: [Midas Typer: implementation of `visit_predicate_stmt`]
) <fig:midas-visit_predicate_stmt>
=== Extend statement <sec:midas-extend-stmt>
#todo[]
=== 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
@@ -362,6 +368,62 @@ Continuing with our example from @fig:example-midas-ast, the type statement woul
caption: [Midas Example: registered type#footnote[Location and position objects are omitted for readability]]
) <fig:example-midas-type>
== Variance inference <sec:variance-inference>
The main `resolve` method of `MidasTyper`, as shown in @fig:midas-typer-resolve and @fig:midas-typer-members, first processes all statements, and then summons a `VarianceManager` to infer variance of all types.
#codly(
range: (68, 78),
smart-skip: true
)
#figure(
midas-typer-members-code,
caption: [Midas Typer: `resolve` method]
) <fig:midas-typer-resolve>
The inference process is actually not very complicated but rigorous. The objective is, for all type variables in all generic types, to walk through all their usages and record their polarity.
By polarity, we mean that:
- any _producer_ position, such as a function return type, is considered *positive*
- any _consumer_ position, such as a function parameter, is considered *negative*
Algorithmically, when inferring the variance of a variable, we start at the root generic type with a positive polarity. The inference function identifies all possible positions (type body and members) and recurses with the current polarity multiplied by the position's polarity. For example, if the current polarity is positive and a variable is used in a producer position, the resulting polarity used when recursing is $+ times + = +$. If however the variable is used in a consumer position, the polarity becomes $+ times - = -$. A consumer or negative position basically _flips_ the current polarity. When the recursion reaches the bottom usage, i.e. a simple `TypeVar`, the polarity is recorded.
This algorithm is implemented by the `VarianceInferrer` class in @fig:midas-variance-inferrer-walk.
#codly(
ranges: (
(1, 2),
(11, 66),
),
smart-skip: true
)
#figure(
raw(block: true, lang: "python", read("../../code/variance_inferrer.py")),
caption: [Implementation of `VarianceInferrer.infer` and `VarianceInferrer.walk`]
) <fig:midas-variance-inferrer-walk>
A `Tracker` helper class is responsible for keeping a record of all occurrences of each type variable, with a list of observed polarities.
When the generic type has been full walked, the tracker returns the list of type variables with their variance fixed, according to the following rule:
- if the variable only appears with positive polarity, it is *covariant*
- if the variable only appears with negative polarity, it is *contravariant*
- 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.
`VarianceManager` is a simple helper class. Its main method, `infer`, is shown in @fig:midas-variance-manager-infer.
#codly(
range: (12, 21),
smart-skip: true
)
#figure(
raw(block: true, lang: "python", read("../../code/variance_manager.py")),
caption: [Implementation of `VarianceManager.infer`]
) <fig:midas-variance-manager-infer>
The complete implementation of all classes mentioned in this section is available in the repository in #code-ref(<midas-variance>, "midas/checker/variance.py").
/*
- Midas definition language
- Lexer + parser (Crafting Interpreters, Pebble)
+66
View File
@@ -0,0 +1,66 @@
Polarity = Literal[-1, 0, 1]
class VarianceInferrer:
def __init__(self, manager: VarianceManager) -> None:
self.manager: VarianceManager = manager
self.tracker: Tracker = Tracker([])
@property
def types(self) -> TypesRegistry:
return self.manager.types
def infer(self, type: GenericType) -> GenericType:
self.tracker = Tracker(type.params)
self.walk(type.body, 1, type.name)
members: dict[str, Member] = self.types._members.get(type.name, {})
for name, member in members.items():
self.walk(member.type, 1, type.name)
return GenericType(
name=type.name,
params=self.tracker.get_updated_vars(),
body=type.body,
)
def walk(
self,
type: Type,
polarity: Polarity,
base_name: str,
):
match type:
case Function(params=spec):
all_params: list[Function.Parameter] = spec.pos + spec.mixed + spec.kw
for param in all_params:
self.walk(
param.type,
-polarity,
base_name,
)
self.walk(type.returns, polarity, base_name)
case OverloadedFunction(overloads=overloads):
for overload in overloads:
self.walk(overload, polarity, base_name)
case AppliedType(name=name, args=args):
if self.manager.is_in_queue(name):
return
generic: Type = self.types.get_type(name)
assert isinstance(generic, GenericType)
generic = self.manager.infer(name, generic)
params: list[TypeVar] = generic.params
polarities: dict[Variance, Polarity] = {
Variance.INVARIANT: 0,
Variance.COVARIANT: 1,
Variance.CONTRAVARIANT: -1,
}
for arg, param in zip(args, params):
param_polarity: Polarity = polarities[param.variance]
self.walk(
arg,
cast(Polarity, polarity * param_polarity),
base_name,
)
case ConstraintType(type=base):
self.walk(base, polarity, base_name)
case TypeVar():
if type in self.tracker:
self.tracker.record(type, polarity)
+27
View File
@@ -0,0 +1,27 @@
class VarianceManager:
def __init__(self, types: TypesRegistry) -> None:
self.types: TypesRegistry = types
self._queue: list[str] = []
self._inferred: set[str] = set()
def infer_all(self):
for name, type in self.types._types.items():
if isinstance(type, GenericType):
self.infer(name, type)
def infer(self, name: str, type: GenericType) -> GenericType:
if self.is_inferred(name):
return type
self._queue.append(name)
inferrer: VarianceInferrer = VarianceInferrer(self)
inferred: GenericType = inferrer.infer(type)
self.types._types[name] = inferred
self._queue.pop()
self._inferred.add(name)
return inferred
def is_in_queue(self, name: str) -> bool:
return name in self._queue
def is_inferred(self, name: str) -> bool:
return name in self._inferred
+28
View File
@@ -0,0 +1,28 @@
class Tracker:
def __init__(self, vars: list[TypeVar]) -> None:
self.vars: list[TypeVar] = vars
self.refs: dict[str, set[Polarity]] = {var.name: set() for var in self.vars}
def record(self, var: TypeVar, polarity: Polarity):
self.refs[var.name].add(polarity)
def get_updated_vars(self) -> list[TypeVar]:
return [
TypeVar(
name=var.name, bound=var.bound, variance=self.get_variance(var.name)
)
for var in self.vars
]
def get_variance(self, name: str) -> Variance:
refs: set[Polarity] = self.refs[name]
if refs == {-1}:
return Variance.CONTRAVARIANT
if refs == {1}:
return Variance.COVARIANT
return Variance.INVARIANT
def __contains__(self, item: TypeVar | str):
if isinstance(item, TypeVar):
return item.name in self
return item in self.refs