This repo showcases a formalization of the type inference of patterns in rust. It is formalized as type inference rules, this repo implements a little solver that applies these typing rules to a given pattern. This can be used to compare alternative rules for typing patterns.
This was built as part of the initiative to improve the rules of match ergonomics. The default settings of the tool is a proposal I (@Nadrieril) am putting forward (though note that this RFC draft is outdated compared to the tool).
The tool is accessible with a web UI at https://nadrieril.github.io/typing-rust-patterns/.
To use the cli tool, run cargo run. It provides an interactive CLI interface with instructions.
Type set to see the various options.
The ruleset in my RFC draft is called stateless in the cli. Other rulesets include
stable rust behavior, RFC3627 behavior, and some alternative proposals.
The tool answers the basic question: can pattern <pattern> work on type <type>, and if so what
types are assigned to the bindings inside <pattern>? Type <pattern>: <type> inside the tool to
get the answer, with reasoning steps.
Available patterns are:
- bindings
x,ref y,mut z, etc - references
&p,&mut p - tuples, written
[p],[p, q]
Available types are:
- variables
T,U, etc - references
&T,&mut T - tuples, written
[T],[T, U]
A query to the tool looks like <pattern>: <type>, which the tool will then attempt to typecheck.
The internal steps however are presented in terms of a more complex predicate, that looks like r, m ⊢ p: T, where:
risinhorrealand indicates whether the outermost reference type (if any) is inherited or not;misrworroand indicates whether we have mutable or read-only access to the original scrutinee;pis a pattern;Tis a type.
The initial predicate will always be real, rw ⊢ <pattern>: <type>. From there, the solver will
apply typing rules.
Type rules to see the current set of typing rules. A rule consists of a list of predicates at the
top called "preconditions", a divider line with the name of the rule, and a list of predicates at
the bottom called "postconditions". To apply a rule, find which postconditions apply to your case
and replace them with the preconditions. Repeat until either no rule applied (this means the input
was a type error), or everything has been resolved into let-bindings.
At the end, you get either a type error or an assignment for all the bindings. The bindings are
assigned a type as well as an expression such as &(*s).0, where s represents the value that was
matched on.
The heart of the solver is a step function with type roughly fn step(RuleSet, Predicate) -> Result<(Rule, Vec<Predicate>), StepError>. It is called repeatedly until success (no predicates
left) or error.
The clever part is that predicates can be partially abstract: we represent an arbitrary pattern p
as Pattern::Abstract. The step function raises TooAbstract if it ever needs to inspect a part
of the predicate that is abstract. If it succeeds, we know that the step that was performed is valid
for any predicate with that shape: this is how we can confidently derive general typing rules from
just that step function.
To derive general typing rules, we start with a fully abstract predicate, and call the step function
on it. As long as it returns TooAbstract, we make the predicate a little bit more precise by
trying all possibilities (e.g. if the pattern is too abstract, we try [p], &p, &mut p and
various bindings). Because the stepping function is careful to only inspect predicates up to a fixed
depth, we eventually get a list of abstract predicates on which the stepping function succeeds, and
which fully describes the behavior of the current ruleset.
We also use this property to speed up comparisons between rulesets: given an abstract predicate, we can make progress on it before needing to split into sub-cases. This means for example that we can prune type errors early.