Skip to content

Instantly share code, notes, and snippets.

@nikomatsakis

nikomatsakis/recursive-solver.md Secret

Last active May 7, 2020
Embed
What would you like to do?

Recursive Solver

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.

Idea of the recursive solver

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".

Contract with existing SLG solver

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.

Downsides of recursive solving

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 ambiguous
  • Implemented(?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].

Upsides of recursive solving

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).

Interaction with associated types

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.

How to make associated types "override"?

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

Distinguishing inputs/outputs

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.)

Priorities

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.

Some examples

Setting

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).

Goal 1: all inputs known

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.

Goal 2: some variables

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.

Precedent: defeasible logics

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.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment