HEL/TB-Docs
1
0
Fork 0
Code Issues Pull Requests Releases Activity
Files
49d5d321c82669f6fa1dffe8b8abe4758e9ef87d
TB-Docs/report/chapters/04_implementation/03_registry.typ

340 lines
18 KiB
Typst
Raw Blame History

#import "../../utils.typ": code-ref
#import "@preview/codly:1.3.0": codly
#import "../../appendices/is_subtype.typ": is-subtype-code, is-func-subtype-code
= 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).
@fig:registry-contract shows the minimal contract our registry must satisfy.
#figure(
```python
class TypesRegistry:
def get_type(self, name: str) -> Type: ...
def define_type(self, name: str, type: Type): ...
def define_member(
self,
type_name: str,
member_name: str,
member_type: Type,
kind: MemberKind,
): ...
def define_predicate(self, name: str, predicate: Predicate): ...
def is_subtype(self, type1: Type, type2: Type) -> bool: ...
def apply_generic(self, type: Type, args: list[Type]) -> Type: ...
def lookup_member(self, type: Type, member_name: str) -> Optional[Type]: ...
def lookup_predicate(self, name: str) -> Optional[Predicate]: ...
```,
caption: [Minimal Registry Contract]
) <fig:registry-contract>
The `define_*` and `lookup_*`/`get_*` methods are quite straightforward, inserting and querying an internal dictionary with some added safeguards and errors to prevent redefining an entity or handle undefined references. Additionally, `define_member` handles overriding methods by wrapping multiple method definitions with the same member name inside an `OverloadedFunction` type. This process is detailed in @sec:define_member hereafter. The complete implementation of `TypesRegistry` is available in the repository in #code-ref(<types-registry>, "midas/checker/registry.py")
== `define_member` <sec:define_member>
#figure(
```python
def define_member(
self,
type_name: str,
member_name: str,
member_type: Type,
kind: MemberKind,
):
members: dict[str, Member] = self._members.setdefault(type_name, {})
if member_name in members:
current: Member = members[member_name]
if current.kind != kind:
self.logger.error(
f"Member '{member_name}' is already defined as a {current.kind},"
+ f" cannot define a {kind} with the same name"
)
return
if kind != MemberKind.METHOD:
self.logger.error(
f"Member '{member_name}' already defined for type {type_name},"
+ " only methods can be overloaded"
)
return
combined: Type
match current.type:
case OverloadedFunction(overloads=overloads):
combined = OverloadedFunction(overloads=overloads + [member_type])
case _:
combined = OverloadedFunction(overloads=[current.type, member_type])
members[member_name] = Member(kind=current.kind, type=combined)
else:
members[member_name] = Member(kind=kind, type=member_type)
```,
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.
== `lookup_member`
`lookup_member` also needs some logic to handle each kind ot types. Indeed, looking up a member on a type (e.g. when processing an attribute reference expression like `foo.bar`), it may be defined in any of the type's supertypes too. Thus the method needs to recurse in the hierarchy if the member cannot be found directly on the requested type.
#figure(
```python
def lookup_member(self, type: Type, member_name: str) -> Optional[Type]:
match type:
case BaseType(name=name):
if name in self._members:
if member_name in self._members[name]:
return self._members[name][member_name].type
return None
case DerivedType(name=name, type=base):
if name in self._members:
if member_name in self._members[name]:
return self._members[name][member_name].type
return self.lookup_member(base, member_name)
case AppliedType(name=name, body=body, args=args):
generic: Type = self.get_type(name)
if not isinstance(generic, GenericType):
raise ValueError("AppliedType not derived from a GenericType")
substitutions = {
type_var.name: arg for arg, type_var in zip(args, generic.params)
}
if name in self._members:
if member_name in self._members[name]:
member_type: Type = self._members[name][member_name].type
return substitute_typevars(member_type, substitutions)
member_type2: Optional[Type] = self.lookup_member(body, member_name)
if member_type2 is not None:
member_type2 = substitute_typevars(member_type2, substitutions)
return member_type2
case ConstraintType(type=base):
return self.lookup_member(base, member_name)
case TypeVar(bound=bound) if bound is not None:
return self.lookup_member(bound, member_name)
case UnknownType():
return UnknownType()
case _:
self.logger.debug(f"Can't get member on {type}")
return None
```
) <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").
== `apply_generic`
`apply_generic` is a simple method which builds an `AppliedType` from a `GenericType` and a list of type arguments. This method is used when processing expressions such as `Foo[Bar]` and is implemented using the aforementioned `substitute_typevars`. Moreover, it checks potential bounds of type parameters. It is also used for the special `TupleType` which is constructed as `tuple[Type1, Type2, ...]`, as shown in @fig:apply_generic.
#figure(
```python
def apply_generic(self, type: Type, args: list[Type]) -> Type:
match type:
case DerivedType(name=name, type=base):
return DerivedType(name=name, type=self.apply_generic(base, args))
case GenericType(name=name, params=type_vars, body=body):
n_args: int = len(args)
n_type_vars: int = len(type_vars)
if n_args < n_type_vars:
raise ValueError(
f"Missing type arguments, expected {n_type_vars} but only {n_args} provided"
)
if n_args > n_type_vars:
raise ValueError(
f"Too many type arguments, expected {n_type_vars} but {n_args} provided"
)
substitutions: dict[str, Type] = {}
for arg, type_var in zip(args, type_vars):
if type_var.bound is not None and not self.is_subtype(
arg, type_var.bound
):
raise ValueError(
f"Type argument {arg} is not a subtype of {type_var.bound}"
)
substitutions[type_var.name] = arg
return AppliedType(
name=name,
args=args,
body=substitute_typevars(body, substitutions),
)
case BaseType(name="tuple"):
return TupleType(items=tuple(args))
case _:
raise ValueError(f"{type} is not a generic type")
```,
caption: [Implementation of `TypesRegistry.apply_generic`]
) <fig:apply_generic>
The first case handling `DerivedType`, @fig:apply_generic:3 to @fig:apply_generic:4, is a kind of syntactic sugar to define subtypes of generic types without redefining and forwarding type parameters, as demonstrated in @fig:generic-subtype.
#figure(
```midas
type Foo[T] = T
type Bar1[T] = Foo[T]
// is functionally equivalent to
type Bar2 = Foo
```,
caption: [Generic subtype syntactic sugar]
) <fig:generic-subtype>
== `is_subtype` <sec:is_subtype>
This method is one of the central parts of our type system. Its role is simple: judge, according to the rules we defined in @sec:typing-subtyping (and some we skipped), whether a given type (`type1`) should be considered a subtype of another (`type2`).
We will first look at the simplest cases and work our way up to the more complex ones. The complete implementation of `is_subtype` is given in @fig:is_subtype#footnote[The order of cases is slightly different from the real implementation for grouped presentation purposes].
The trivial case where `type1` is the same as `type2` can be handled with a simple equality check, which is implemented by the `dataclasses` module (#smallcaps[S-Refl] in @tab:typing-subtyping-base). This is the first check in the method, as shown in @fig:is_subtype-equal.
#codly(
range: (1, 3),
smart-skip: true
)
#figure(
is-subtype-code,
caption: [`is_subtype`: equal types]
) <fig:is_subtype-equal>
Even if the types differ, some cases such as top types are still trivially handled. If `type2` is a top type, `type1` is by definition a subtype (#smallcaps[S-Any] and #smallcaps[S-Unknown] in @tab:typing-subtyping-top).
#codly(
ranges: ((5, 10), (71, 71)),
smart-skip: true
)
#figure(
is-subtype-code,
caption: [`is_subtype`: top types]
) <fig:is_subtype-top>
For builtin types, we define some hardcoded subtype relationships, which are checked if both types are instances of `BaseType`. It may happen one or both of the types are type variables. If that is the case and the type variable has a bound, we may recursively check the subtype relationship against the bound. If not, we cannot make any assumption about the type of the variable and must return `False`. @fig:is_subtype-base-vars shows how both these cases are handled.
#codly(
range: (12, 23),
smart-skip: true
)
#figure(
is-subtype-code,
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).
The implementation shown in @fig:is_subtype-derived-constr is a straightforward application of these rules.
#codly(
range: (25, 29),
smart-skip: true
)
#figure(
is-subtype-code,
caption: [`is_subtpye`: derived and constraint types]
) <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:
- 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
This verification is implemented as in @fig:is_subtype-applied-type.
#codly(
range: (31, 50),
smart-skip: true
)
#figure(
is-subtype-code,
caption: [`is_subtype`: applied types]
) <fig:is_subtype-applied-type>
The second case simply handles other situations where `type1` is an `AppliedType`, recursively checking its body against `type2` similarly to derived types.
Only three rules remain to check for dataframes, columns and most importantly functions.
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.
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.
#codly(
range: (51, 69),
smart-skip: true
)
#figure(
is-subtype-code,
caption: [`is_subtype`: dataframes, columns and functions]
) <fig:is_subtype-df-cols-funcs>
== `is_func_subtype` <sec:is_func_subtype>
This section describes the implementation of the function subtyping verification algorithm. Please refer to @app:function-subtyping for more information on the underlying theory and formal rules.
The complete implementation of `is_func_subtype` is given in @fig:is_func_subtype.
The first thing `is_func_subtype` must check is whether the return types of the given functions are subtypes of one another (see #smallcaps[S-Func] in @tab:typing-subtyping-function). A simple early return can be added right at the beginning of the method, as shown in @fig:is_func_subtype-returns.
#codly(
range: (1, 3),
smart-skip: true
)
#figure(
is-func-subtype-code,
caption: [`is_func_subtype`: check return types]
) <fig:is_func_subtype-returns>
As we will need to get parameters of each function by kind, name and position, we will first extract the different lists and dictionaries in short variables as outlined in @fig:is_func_subtype-extract-params. These correspond to $(P_1, M_1, K_1)$ and $(P_2, M_2, K_2)$ in the theoretical description.
#codly(
range: (5, 22),
smart-skip: true
)
#figure(
is-func-subtype-code,
caption: [`is_func_subtype`: extracting parameters]
) <fig:is_func_subtype-extract-params>
We first check that `func2`'s positional- and keyword-only parameters are appropriately covered by `func1`. We also record parameter matches to later check subtyping between them and additional parameters of `func1`.
@fig:is_func_subtype-pos-kw shows how this is implemented with simple loops.
#codly(
range: (24, 52),
smart-skip: true
)
#figure(
is-func-subtype-code,
caption: [`is_func_subtype`: checking positional- and keyword-only parameters]
) <fig:is_func_subtype-pos-kw>
Verifying proper coverage of mixed arguments is slightly more complicated but a similar method can be used to implement the theoretical algorithm, such as in @fig:is_func_subtype-mixed.
#codly(
range: (54, 80),
smart-skip: true
)
#figure(
is-func-subtype-code,
caption: [`is_func_subtype`: checking mixed parameters]
) <fig:is_func_subtype-mixed>
Finally in @fig:is_func_subtype-extra-subtypes, we check that `func1` does not introduce new required parameters and that matching parameters respect contravariance.
#codly(
range: (82, 98),
smart-skip: true
)
#figure(
is-func-subtype-code,
caption: [`is_func_subtype`: check extra parameters and subtypes]
) <fig:is_func_subtype-extra-subtypes>
Reference in New Issue View Git Blame Copy Permalink