Chalk: The High-level Design Plan

Core idea

The core idea of Chalk is to “compile” Rust trait/impl declarations into an intermediate form. The specific intermediate form is Prolog-style clauses — actually, an extended form called “hereditary harrop clauses”. Like any IR, making this change can simplify things, because now we can separate two problems that were previously entangled:

  • How to “solve” traits — i.e., determine whether a trait is implemented for some set of types, figure out the normalized form of an associated type, etc
  • How to “define” the semantics of Rust traits — this is done by the logical lowering

The 10,000 mile view

We want to separate out the trait solver into an independent component from the rest of rustc:

/--------------\ <- Program clauses P <- /-----------\
| Trait Solver | <- Query Goals <------- | rustc     |
\--------------/ ----> Query Results --> \-----------/

  • rustc creates program clauses P from the Rust source:
  • A program clause is basically a logical inference rule:
  • It says “if you know X and Y are true, then you can conclude Z is true too”.
  • This is a process analogous to HIR lowering
  • In particular, like HIR lowering, it is (largely) a mechanical and local process that converts each trait and impl into a set of program clauses. 
  • These program clauses are fed to the trait solver.
  • While doing type-checking, the rustc compiler can then ask the trait solver to prove goals:
  • A goal is just a logical predicate that can be tested against the program clauses P
  • It can include unknown variables, and the trait solver will enumerate possible values for those variables.
  • The solver knows nothing about Rust per se.
  • Details of the solver:
  • The solver yields up one answer at a time. Ultimately, it can enumerate all possible solutions.
  • If you ask it, for example, to solve ?T: Clone, it would eventually try to enumerate all clone-able types that exist.
  • However, it can also stop at any time.
  • It uses a breadth-first-esque search policy, so if solving ?T: Clone, it might first produce ?T = u32 and then ?T = Vec<u32> etc. 
  • Since the compiler, for the most part, only cares about unique answers, we can typically stop the search quite early.
  • But the details of the search are going to be an important detail to work out.

Basic idea of program clause lowering

Here we present a somewhat simplified example of how program clause lowering can look. In fact, the formulation given here is not enough, particularly if we want to support implied bounds — but it should give you a flavor. For more details on the actual lowering rules, you can check out the rustc-guide, although the details and notation there a bit outdated .There is also this DropBox paper that is attempting to sketch out newer rules. (Also, note that the presentation here is similar to what was described in the Lowering Rust Traits To Logic blog post.) 

To start, let’s define a very simple kind of predicate. We’ll call this a domain goal, meaning “something we might want to prove”. We’ll start with just one sort of domain goal, Implemented[Trait], where Trait is the name of some trait (e.g., Implemented[Sized] or Implemented[Clone]). This predicate is applied to the parameters of the trait; so Implemented[Clone](u32) would mean u32: Clone in Rust notation. We might define the grammar sort of like this:

DomainGoal := Implemented[TraitId](P0..Pn)
           |  ...

// A parameter "P" is either a type or a lifetime
P := <type> | <lifetime>

// A "TraitId" is the name of a trait -- or, in Rustc, a `DefId`.
// These are pulled out because you can't (at least presently) have goals like
// `forall<Trait> { ... }` (i.e., you cannot quantify over traits).
TraitId := <trait id>

Now imagine this Rust program: