Type Tailoring without Macros
The dream would be to build a flexible type system that can verify any dynamic program. But we are not quite there yet - mostly because of the non-disjoint nature of data in these programs. Dynamic languages allow types to overlap with one another (for example, in Python a value can be both a string and an iterable), making it nearly intractable for current type checkers to reason about every possible type relationship1. Until we can resolve these relationships in some reasonable amount of time, it might be worth exploring developer-assisted approaches to assist type checking with our current systems.
One such approach is type tailoring2. Type tailoring is a way to for languages with macro systems to introduce domain-specific typing rules. However, the same goal could be realized with modular type checkers with a plugin interface such as Mypy3 that allow developers to extend the type system with domain-specific constructs.
This piece introduces Mypy Plugins and covers some interesting use cases for it: (1) introducing inference support for the Lazy evaluation pattern, and (2) an idealistic idea to preprocess type annotations to safeguard values tagged with the dynamic type (any).
Lazy evaluation inference
The Lazy evaluation pattern is commonplace within the python community for delaying the instantiation of objects until they are needed. This approach optimizes memory by lazily creating objects only when they are required instead of eager initialization at module import time. Type information for this lazy object cannot be available at compile time which makes type checkers unable to verify programs that include such constructs. Language idioms such as this present challenges for gradual type checkers, often forcing developers to fall back to the Any type, which weakens overall soundness guarantees.
Consider this code sample of lazy object instantiation:
|
|
Mypy fails to recognize that foo()
is a method of our lazily instantiated object. By running Mypy’s special function to display the inferred static type of an expression,
reveal_type(lazy_inst.foo())
, we see Mypy resorts to Any
(the dynamic type) instead of capturing None
as the return type.
|
|
This means we lose precision about our lazy object and further interactions with the object just propagate
the Any
type all up our type analysis.
This is where our Mypy plugin would come in handy. By implementing attribute hooks4, we can teach Mypy how to correctly type
lazy objects. These hooks intercept attribute lookups during static analysis, allowing us to provide Mypy
with the actual types that will be available at runtime. For our lazy object, we’ll create a plugin that
tells Mypy that any attribute access on our lazy object should resolve to the types of the underlying NewObj
instance.
|
|
When we call reveal_type again, Mypy correctly identifies lazy_inst.foo() as returning None, giving us proper type safety for our lazy instantiation pattern.
|
|
Preprocessing Type Hints
In the rest of this post, I attempt employing Mypy plugins to preprocess type annotations dynamically. For instance, consider a poorly typed function returning Any
instead of a more specific type like str
. We can implement plugin hooks that detect such patterns and nudge type inferencer to better reflect the function’s behaviour during type checking.
|
|
To achieve this, FILL.
Github Issues that highlight this problem. TypeScript, Luau and Mypy. ↩︎
You can check out the OG paper about Type Tailoring with Macros ↩︎
Mypy is a static type checker for Python that comes with a plugin system (see: plugin.py) ↩︎
Attribute Hooks are a mechanism in the Plugin API that allow you to customize how Mypy handles attribute accesses within your code. Some other mechanism include function and method hooks, class hooks, etc. (see more). ↩︎