Some notes on an idea for recursive trait solver. Note that the term "recursive solver" is not a standard term, I'm just inventing it.
rustc currently uses a "recursive" solver, and we used to have one in chalk, but we moved away from it. The idea of a recursive solver is that you give it a goal G to solve and it gives you back one answer, A. In particular, that answer A must be unambiguous.
Consider a trait with two impls:
trait Scalar32 { }
impl Scalar32 for u32 { }
impl Scalar32 for i32 { }
impl Scalar32 for f32 { }
If we ask the recursive solver to solve the goal Implemented(?X: Scalar32), where ?X indicates an inference variable, it will simply
respond with "ambigiuous".
In contrast, the existing SLG solver gives back many answers that must
be explored one by one, and then gives the caller the job of figuring
out if they are unambiguous. When we ask a query like Implemented(?X: Scalar32), we in get back a stream (or iterator) of answers, where we
can decide how many times to pull on that stream. In this case the
stream would yield the following answers (in some undefined order)
before indicating that there are no more answers remaining:
[?X = u32][?X = i32][?X = f32]
Under the SLG model, it is then the job of the one asked for answers
to decide what to do with ambiguity. In our solver, we will pursue a
single answer (e.g., [?X = u32]) through various intermediate goals,
but if we find ambiguity at the top level, we will stop asking for
more answers.
So, if we were asking Implemented(?X: Scalar32) as our "root query", we
would stop after getting back the second answer, since it would be
clear there is no unambiguous result.
The primary downside of recursive solving is that it is less
"complete". That is, sometimes it can fail to find answers that
exist, and instead results in ambiguity (the same is true of our SLG
solver, mind, but in much narrower circumstances). To see where they
differ, consider a trait like Combine, which builds on the Scalar32
example we had before:
trait Combine { }
impl<T> Combine for T
where
T: Scalar32 + SignedInt
{ }
trait SignedInt { }
impl SignedInt for i16 { }
impl SignedInt for i32 { }
impl SignedInt for i64 { }
Now imagine a query like Implemented(?T: Combine). The recursive
solver would start by finding the impl for Combine and
then recursively attempting to solve:
Implemented(?T: Scalar32)-- yields ambiguousImplemented(?T: SignedInt)-- yields ambiguous
Since neither of the "subgoals" was able to make any progress, it would give up and yield an ambiguous result overall.
In contrast, the SLG solver would recursively attempt to solve
Implemented(?T: Scalar32), and it would iterate through the answers
one by one. Of the three answers (u32, i32, f32), only one of
them would also for ?T: SignedInt, and hence it would find that
the answer is [?T = i32].
The upside of recursive solving is reasonably clear. It never attempts to iterate as deeply through options, so it does overall a lot less work, and it ultimately stores a lot less data.
It also has a structure that is more compatible with inserting more complex logic, and possibly with integration into a salsa-like query system, since solving a single query is more like a subroutine (though there is some complexity I'm glossing over for the moment around "tabling", which basically means in the case of cycles we may have to run the solver routine more than once to reach a fixed point).
We used to have a recursive solver. We abandoned it both because of
its general incompleteness (described above) but in particular
because of a bad interaction with the way we model associated
types. Consider the ProjectionEq rules, which have a normalize
clause and a placeholder clause:
ProjectionEq(<?T as Foo>::Bar = ?U) :-
Normalize(<?T as Foo>::Bar -> ?U).
ProjectionEq(<?T as Foo>::Bar = ?U) :-
Implemented(?T: Foo),
?U = !<?T as Foo>::Bar.
Now imagine that we try to solve something where we actually know the
impl, like projection Iterator::Item from vec::IntoIter<u32>,
which should yield u32:
ProjectionEq(<vec::IntoIter<u32> as Iterator>::Item = ?U)
In this case, the recursive solver is going to wind up with two
answers: u32 and the placeholder. Therefore, it's going to yield
ambiguous.
I was contemplating ways to resolve the associated type normalization problem. Basically I think we want some way to know that, if we have an answer from an impl that is equally general, it will 'override' the placeholder answer. (rustc implements a similar rule, although I think it is has various bugs.)
I have a vague plan but it involves two concepts working together:
- distinguishing inputs/outputs and
- priorities
In our notion of domain goals today, we don't distinguish anything
about the parameters. So you might have a domain goal like this, where
we use _ to indicate each of the parameters to the goal:
ProjectionEq(<_ as Iterator>::Item = _)
However, we could say that domain goals can optionally have an
output parameter. Specifically, all ProjectionEq and Normalize
goals would declare the resulting type to be the "output":
ProjectionEq(<_ as Iterator>::Item = _)
// ^ input ^ output
ProjectionEq(<_ as Foo<_>>::Bar = _)
// ^ input ^ input ^ output
Normalize(<_ as Iterator>::Item = _)
// ^ input ^ output
Normalize(<_ as Foo<_>>::Bar = _)
// ^ input ^ input ^ output
On its own, the input/output distinction is not very meaningful. It becomes useful when combined with priorities.
(Note: the intuition for declaring something to be an output is that, given the same inputs, all possible values for the output you can find will be semantically equivalent. But this is not strictly required, I don't think, which is good -- because via where clauses users can violate this property.)
We can next have the idea of "lower priority" rules. The idea here is that most program clauses are "high priority" but we declare some clauses to be "low priority". If you have both a high and a low priority clause where all input parameters have equal values, you can discard the answer derived from the lower priority rule. Note that the outputs do not have to be the same.
We would use this for the "placeholder" rule:
// high priority:
ProjectionEq(<?T as Foo>::Bar = ?U) :-
Normalize(<?T as Foo>::Bar -> ?U).
// low priority:
ProjectionEq(<?T as Foo>::Bar = ?U) :-
?U = !<?T as Foo>::Bar.
Consider this trait and impl:
trait Foo<T> {
type Bar;
}
impl Foo<u32> for i32 {
type Bar = f32;
}
These would give rise to the following program clauses:
// From the trait:
ProjectionEq(<?Self as Foo<?T>>::Bar = ?U) :-
Normalize(<?Self as Foo<?T>>::Bar = ?U).
// Low priority
ProjectionEq(<?Self as Foo<?T>>::Bar = ?U) :-
Implemented(?Self: Foo<?T>),
?U = !<?Self as Foo<?T>>::Bar.
// From the impl:
Implemented(i32: Foo<u32>).
Normalize(<i32 as Foo<u32>>::Bar = f32).
Now imagine we were trying to prove the following goal
ProjectionEq(<i32 as Foo<u32>>::Bar = ?X)
We start by searching the "high priority" rules for an answer, and we
find ?X = f32. We next search the low priority rules and we find
another answer, but we can discard it, as all the inputs are the same,
and only the output differs.
Next imagine we were trying to prove the following goal, where one of the inputs is not known:
ProjectionEq(<i32 as Foo<?A>>::Bar = ?X)
This is trickier. The high priority rule would generate this answer:
[?A = u32, ?X = f32]
but the low priority rules would generate an answer that does not
constrain the input ?A:
[?X = !<i32 as Foo<?A>>::Bar]
In this case, the high priority answer does not overrule the low priority one, because the inputs are not equal.
We would therefore ultimately get back an ambiguous result here,
becaus we have two conflicting answers at this point. Note that I
think rustc would take the first answer, even though that is not as
general a result as you could have. The chalk equivalent would be that
we might give guidance suggesting that ?A = u32 would be a good
type hint.
Both the concept of 'priorities' and inputs and outputs have various bits of precedent that are worth reviewing and looking more into. Off the top of my head:
For inputs/outputs, many prologs have various kinds of 'modes' that express similar concepts, though they don't generally capture the idea that, given the same inputs, you will have equivalent values for the outputs. In fact, the modes in prologs I think are more oriented around the idea that we express as "floundering" -- i.e., if you have "input" parameters, then their values must be known or else the rule cannot usefully enumerate their possible values.
The uniqueness concepts (which aren't really critical, as I wrote) are more similar to functional dependencies and associated types. But this uniqueness is really more to do with the Rust language and is enforced by coherence.
The notion of priorities is related to defeasible logics, where you have the idea of general rules ("all birds can fly") whose conclusions can be deafeated by more narrow ones ("but penguins cannot"). There are some people who've looked into those in a Prolog context. I have to go review some of this stuff to see if it offers any insights. (It's also, as it happens, related to modeling specialization.)