|
| 1 | +# Judgment functions and inference rules |
| 2 | + |
| 3 | +The next thing is the `judgement_fn!` macro. This lets you write a *judgment* using *inference rules*. A "judgment" just means some kind of predicate that the computer can judge to hold or not hold. Inference rules are those rules you may have seen in papers and things: |
| 4 | + |
| 5 | +``` |
| 6 | +premise1 |
| 7 | +premise2 |
| 8 | +premise3 |
| 9 | +------------------ |
| 10 | +conclusion |
| 11 | +``` |
| 12 | + |
| 13 | +i.e., the conclusion is judged to be true if all the premises are true. |
| 14 | + |
| 15 | +[`prove_wc`]: https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-prove/src/prove/prove_wc.rs#L21-L125 |
| 16 | + |
| 17 | +Judgments in type system papers can look all kinds of ways. For example, a common type system judgment would be the following: |
| 18 | + |
| 19 | +``` |
| 20 | +Γ ⊢ E : T |
| 21 | +``` |
| 22 | + |
| 23 | +This can be read as, in the environment Γ, the expression E has type T. You might have rule like these: |
| 24 | + |
| 25 | +``` |
| 26 | +Γ[X] = ty // lookup variable in the environment |
| 27 | +--------------- "variable" |
| 28 | +Γ ⊢ X : ty |
| 29 | +
|
| 30 | +Γ ⊢ E1 : T // must have the same type |
| 31 | +Γ ⊢ E2 : T |
| 32 | +--------------- "add" |
| 33 | +Γ ⊢ E1 + E2 : T |
| 34 | +``` |
| 35 | + |
| 36 | +In a-mir-formality, you might write those rules like so: |
| 37 | + |
| 38 | +```rust |
| 39 | +judgment_fn! { |
| 40 | + pub fn has_type( |
| 41 | + env: Env, |
| 42 | + expr: Expr, |
| 43 | + ) => Type { |
| 44 | + ( |
| 45 | + (env.get(&name) => ty) |
| 46 | + --------------- |
| 47 | + (has_type(env, name: Variable) => ty) |
| 48 | + ) |
| 49 | + |
| 50 | + ( |
| 51 | + (has_type(env, left) => ty_left) |
| 52 | + (has_type(env, right) => ty_right) |
| 53 | + (if ty_left == ty_right) |
| 54 | + --------------- |
| 55 | + (has_type(env, Expr::Add(left, right)) => ty_left) |
| 56 | + ) |
| 57 | + } |
| 58 | +} |
| 59 | +``` |
| 60 | + |
| 61 | +Unlike mathematical papers, where judgments can look like whatever you want, judgments in a-mir-formality always have a fixed form that distinguish inputs and outputs: |
| 62 | + |
| 63 | +``` |
| 64 | +judgment_name(input1, input2, input3) => output |
| 65 | +``` |
| 66 | + |
| 67 | +In this case, `has_type(env, expr) => ty` is the equivalent of `Γ ⊢ E : T`. Note that, by convention, we tend to use more English style names, so `env` and not `Γ`, and `expr` and not `E`. Of course nothing is stop you from using single letters, it's just a bit harder to read. |
| 68 | + |
| 69 | +When we write the `judgement_fn`, it is going to desugar into an actual Rust function that looks like this: |
| 70 | + |
| 71 | +```rust |
| 72 | +pub fn has_type(arg0: impl Upcast<Env>, arg1: impl Upcast<Expr>) -> Set<Type> { |
| 73 | + let arg0: Env = arg0.upcast(); |
| 74 | + let arg1: Expr = arg1.upcast(); |
| 75 | + |
| 76 | + ... |
| 77 | +} |
| 78 | +``` |
| 79 | + |
| 80 | +Some things to note. First, the function arguments (`arg0`, `arg1`) implicitly accept anything that "upcasts" (infallibly converts) into the desired types. `Upcast` is a trait defined within a-mir-formality and implemented by the `#[term]` macro automatically. |
| 81 | + |
| 82 | +Second, the function always returns a `Set`. This is because there can be more rules, and they may match in any ways. The generated code is going to exhaustively search to find all the ways that the rules could match. At a high-level the code looks like this (at least if we ignore the possibility of cycles; we'll come back to that later): |
| 83 | + |
| 84 | +```rust |
| 85 | +pub fn has_type(arg0: impl Upcast<Env>, arg1: impl Upcast<Expr>) -> Set<Type> { |
| 86 | + let arg0: Env = arg0.upcast(); |
| 87 | + let arg1: Expr = arg1.upcast(); |
| 88 | + |
| 89 | + let mut results = set![]; // we define this macro |
| 90 | + |
| 91 | + if /* inference rule 1 matches */ { |
| 92 | + results.push(/* result from inference rule 1 */); |
| 93 | + } |
| 94 | + |
| 95 | + if /* inference rule 2 matches */ { |
| 96 | + results.push(/* result from inference rule 1 */); |
| 97 | + } |
| 98 | + |
| 99 | + // ... |
| 100 | + |
| 101 | + if /* inference rule N matches */ { |
| 102 | + results.push(/* result from inference rule N */); |
| 103 | + } |
| 104 | + |
| 105 | + results |
| 106 | +} |
| 107 | +``` |
| 108 | + |
| 109 | +So how do we test if a particular inference rule matches? Let's look more closely at the code we would generate for this inference rule: |
| 110 | + |
| 111 | +```rust |
| 112 | +( |
| 113 | + (env.get(name) => ty) |
| 114 | + --------------- |
| 115 | + (has_type(env, name: Variable) => ty) |
| 116 | +) |
| 117 | +``` |
| 118 | + |
| 119 | +The first part of the final line, `has_type(env, name: Variable)`, defines patterns that are matched against the arguments. These are matched against the arguments (`arg0`, `arg1`) from the judgment. Patterns can either be trivial bindings (like `env`) or more complex (like `name: Variable` or `Expr::Add(left, right)`). In the latter case, they don't have to match the type of the argument precisely. Instead, we use the `Downcast` trait combined with pattern matching. So this inference rule would compile to something like... |
| 120 | + |
| 121 | +```rust |
| 122 | +// Simple variable bindings just clone... |
| 123 | +let env = arg0.clone(); |
| 124 | + |
| 125 | +// More complex patterns are downcasted and testing... |
| 126 | +if let Some(name) = arg1.downcast::<Variable>() { |
| 127 | + ... // rule successfully matched! See below. |
| 128 | +} |
| 129 | +``` |
| 130 | + |
| 131 | +Once we've matched the arguments, we start trying to execute the inference rule conditions. We have one, `env.get(&name) => ty`. What does that do? A condition written like `$expr => $pat` basically becomes a for loop, so you get... |
| 132 | + |
| 133 | +```rust |
| 134 | +let env = arg0.clone(); |
| 135 | +if let Some(name) = arg1.downcast::<Variable>() { |
| 136 | + for ty in env.get(&name) { |
| 137 | + ... // other conditions, if any |
| 138 | + } |
| 139 | +} |
| 140 | +``` |
| 141 | + |
| 142 | +Once we run out of conditions, we can generate the final result, which comes from the `=> $expr` in the conclusion of the rule. In this case, something like this: |
| 143 | + |
| 144 | +```rust |
| 145 | +let env = arg0.clone(); |
| 146 | +if let Some(name) = arg1.downcast::<Variable>() { |
| 147 | + for ty in env.get(&name) { |
| 148 | + result.push(ty); |
| 149 | + } |
| 150 | +} |
| 151 | +``` |
| 152 | + |
| 153 | +Thus each inference rule is converted into a little block of code that may push results onto the final set. |
| 154 | + |
| 155 | +The second inference rule (for addition) looks like... |
| 156 | + |
| 157 | +```rust |
| 158 | +// given this... |
| 159 | +// ( |
| 160 | +// (has_type(env, left) => ty_left) |
| 161 | +// (has_type(env, right) => ty_right) |
| 162 | +// (if ty_left == ty_right) |
| 163 | +// --------------- |
| 164 | +// (has_type(env, Expr::Add(left, right)) => ty_left) |
| 165 | +// ) |
| 166 | +// we generate this... |
| 167 | +let env = arg0.clone(); |
| 168 | +if let Some(Expr::Add(left, right)) = arg1.downcast() { |
| 169 | + for ty_left in has_type(env, left) { |
| 170 | + for ty_right in has_type(env, right) { |
| 171 | + if ty_left == ty_right { |
| 172 | + result.push(ty_left); |
| 173 | + } |
| 174 | + } |
| 175 | + } |
| 176 | +} |
| 177 | +``` |
| 178 | + |
| 179 | +If you want to see a real judgement, take a look at the one for [proving where clauses][`prove_wc`]. |
| 180 | + |
| 181 | +[`prove_wc`]: https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-prove/src/prove/prove_wc.rs#L21-L125 |
| 182 | + |
| 183 | +### Handling cycles |
| 184 | + |
| 185 | +Judgment functions must be **inductive**, which means that cycles are considered failures. We have a tabling implementation, which means we detect cycles and try to handle them intelligently. Basically we track a stack and, if a cycle is detected, we return an empty set of results. But we remember that the cycle happened. Then, once we are done, we'll have computed some intermediate set of results `R[0]`, and we execute again. This time, when we get the cycle, we return `R[0]` instead of an empty set. This will compute some new set of results, `R[1]`. So then we try again. We keep doing this until the new set of results `R[i]` is equal to the previous set of results `R[i-1]`. At that point, we have reached a fixed point, so we stop. Of course, it could be that you get an infinitely growing set of results, and execution never terminates. This means your rules are broken. Don't do that. |
0 commit comments