src/doc/rustc-guide/src/traits/lowering-to-logic.md

   1 # Lowering to logic
   2
   3 The key observation here is that the Rust trait system is basically a
   4 kind of logic, and it can be mapped onto standard logical inference
   5 rules. We can then look for solutions to those inference rules in a
   6 very similar fashion to how e.g. a [Prolog] solver works. It turns out
   7 that we can't *quite* use Prolog rules (also called Horn clauses) but
   8 rather need a somewhat more expressive variant.
   9
  10 [Prolog]: https://en.wikipedia.org/wiki/Prolog
  11
  12 ## Rust traits and logic
  13
  14 One of the first observations is that the Rust trait system is
  15 basically a kind of logic. As such, we can map our struct, trait, and
  16 impl declarations into logical inference rules. For the most part,
  17 these are basically Horn clauses, though we'll see that to capture the
  18 full richness of Rust – and in particular to support generic
  19 programming – we have to go a bit further than standard Horn clauses.
  20
  21 To see how this mapping works, let's start with an example. Imagine
  22 we declare a trait and a few impls, like so:
  23
  24 ```rust
  25 trait Clone { }
  26 impl Clone for usize { }
  27 impl<T> Clone for Vec<T> where T: Clone { }
  28 ```
  29
  30 We could map these declarations to some Horn clauses, written in a
  31 Prolog-like notation, as follows:
  32
  33 ```text
  34 Clone(usize).
  35 Clone(Vec<?T>) :- Clone(?T).
  36
  37 // The notation `A :- B` means "A is true if B is true".
  38 // Or, put another way, B implies A.
  39 ```
  40
  41 In Prolog terms, we might say that `Clone(Foo)` – where `Foo` is some
  42 Rust type – is a *predicate* that represents the idea that the type
  43 `Foo` implements `Clone`. These rules are **program clauses**; they
  44 state the conditions under which that predicate can be proven (i.e.,
  45 considered true). So the first rule just says "Clone is implemented
  46 for `usize`". The next rule says "for any type `?T`, Clone is
  47 implemented for `Vec<?T>` if clone is implemented for `?T`". So
  48 e.g. if we wanted to prove that `Clone(Vec<Vec<usize>>)`, we would do
  49 so by applying the rules recursively:
  50
  51 - `Clone(Vec<Vec<usize>>)` is provable if:
  52   - `Clone(Vec<usize>)` is provable if:
  53     - `Clone(usize)` is provable. (Which it is, so we're all good.)
  54
  55 But now suppose we tried to prove that `Clone(Vec<Bar>)`. This would
  56 fail (after all, I didn't give an impl of `Clone` for `Bar`):
  57
  58 - `Clone(Vec<Bar>)` is provable if:
  59   - `Clone(Bar)` is provable. (But it is not, as there are no applicable rules.)
  60
  61 We can easily extend the example above to cover generic traits with
  62 more than one input type. So imagine the `Eq<T>` trait, which declares
  63 that `Self` is equatable with a value of type `T`:
  64
  65 ```rust,ignore
  66 trait Eq<T> { ... }
  67 impl Eq<usize> for usize { }
  68 impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }
  69 ```
  70
  71 That could be mapped as follows:
  72
  73 ```text
  74 Eq(usize, usize).
  75 Eq(Vec<?T>, Vec<?U>) :- Eq(?T, ?U).
  76 ```
  77
  78 So far so good.
  79
  80 ## Type-checking normal functions
  81
  82 OK, now that we have defined some logical rules that are able to
  83 express when traits are implemented and to handle associated types,
  84 let's turn our focus a bit towards **type-checking**. Type-checking is
  85 interesting because it is what gives us the goals that we need to
  86 prove. That is, everything we've seen so far has been about how we
  87 derive the rules by which we can prove goals from the traits and impls
  88 in the program; but we are also interested in how to derive the goals
  89 that we need to prove, and those come from type-checking.
  90
  91 Consider type-checking the function `foo()` here:
  92
  93 ```rust,ignore
  94 fn foo() { bar::<usize>() }
  95 fn bar<U: Eq<U>>() { }
  96 ```
  97
  98 This function is very simple, of course: all it does is to call
  99 `bar::<usize>()`. Now, looking at the definition of `bar()`, we can see
 100 that it has one where-clause `U: Eq<U>`. So, that means that `foo()` will
 101 have to prove that `usize: Eq<usize>` in order to show that it can call `bar()`
 102 with `usize` as the type argument.
 103
 104 If we wanted, we could write a Prolog predicate that defines the
 105 conditions under which `bar()` can be called. We'll say that those
 106 conditions are called being "well-formed":
 107
 108 ```text
 109 barWellFormed(?U) :- Eq(?U, ?U).
 110 ```
 111
 112 Then we can say that `foo()` type-checks if the reference to
 113 `bar::<usize>` (that is, `bar()` applied to the type `usize`) is
 114 well-formed:
 115
 116 ```text
 117 fooTypeChecks :- barWellFormed(usize).
 118 ```
 119
 120 If we try to prove the goal `fooTypeChecks`, it will succeed:
 121
 122 - `fooTypeChecks` is provable if:
 123   - `barWellFormed(usize)`, which is provable if:
 124     - `Eq(usize, usize)`, which is provable because of an impl.
 125
 126 Ok, so far so good. Let's move on to type-checking a more complex function.
 127
 128 ## Type-checking generic functions: beyond Horn clauses
 129
 130 In the last section, we used standard Prolog horn-clauses (augmented with Rust's
 131 notion of type equality) to type-check some simple Rust functions. But that only
 132 works when we are type-checking non-generic functions. If we want to type-check
 133 a generic function, it turns out we need a stronger notion of goal than what Prolog
 134 can provide. To see what I'm talking about, let's revamp our previous
 135 example to make `foo` generic:
 136
 137 ```rust,ignore
 138 fn foo<T: Eq<T>>() { bar::<T>() }
 139 fn bar<U: Eq<U>>() { }
 140 ```
 141
 142 To type-check the body of `foo`, we need to be able to hold the type
 143 `T` "abstract".  That is, we need to check that the body of `foo` is
 144 type-safe *for all types `T`*, not just for some specific type. We might express
 145 this like so:
 146
 147 ```text
 148 fooTypeChecks :-
 149   // for all types T...
 150   forall<T> {
 151     // ...if we assume that Eq(T, T) is provable...
 152     if (Eq(T, T)) {
 153       // ...then we can prove that `barWellFormed(T)` holds.
 154       barWellFormed(T)
 155     }
 156   }.
 157 ```
 158
 159 This notation I'm using here is the notation I've been using in my
 160 prototype implementation; it's similar to standard mathematical
 161 notation but a bit Rustified. Anyway, the problem is that standard
 162 Horn clauses don't allow universal quantification (`forall`) or
 163 implication (`if`) in goals (though many Prolog engines do support
 164 them, as an extension). For this reason, we need to accept something
 165 called "first-order hereditary harrop" (FOHH) clauses – this long
 166 name basically means "standard Horn clauses with `forall` and `if` in
 167 the body". But it's nice to know the proper name, because there is a
 168 lot of work describing how to efficiently handle FOHH clauses; see for
 169 example Gopalan Nadathur's excellent
 170 ["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
 171 in [the bibliography].
 172
 173 [the bibliography]: ./bibliography.html
 174 [pphhf]: ./bibliography.html#pphhf
 175
 176 It turns out that supporting FOHH is not really all that hard. And
 177 once we are able to do that, we can easily describe the type-checking
 178 rule for generic functions like `foo` in our logic.
 179
 180 ## Source
 181
 182 This page is a lightly adapted version of a
 183 [blog post by Nicholas Matsakis][lrtl].
 184
 185 [lrtl]: http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/