Type Classes as Logic Programs

Type class systems are logic languages. A specific set of trait definitions and implementors form a logic program. Trait resolution then evaluates the constructed program and is implemented as a backtracking search. We reduce trait resolution to logic programming to emphasize problem structure. This problem is not inherent to Rust per say, but a broader complexity coming from this evaluation style. Logic languages provide a language-agnostic way to discuss type class systems. By abstracting away Rust-specific details we highlight that this problem is inherent to any type class implementation reducible to logic program evaluation.

To explore the difference between the good and poor diagnostics of the previous section we will turn each set of traits and implementations into a logic program. We then interpret a query over this program to simulate trait resolution.

Our toy example motivating the need for type class abstraction, the ToString trait, produced a good diagnostic. Let us step through the structure of this program one more time, but instead we will focus on the declarative semantics of the trait language.

trait ToString
{ /*...*/ }

impl ToString for i32
{ /*...*/ }

impl ToString for char
{ /*...*/ }

impl<T> ToString for Vec<T>
where
  T: ToString,
{ /*...*/ }

to_string(i32).

to_string(char).

to_string(vec(T)) :-
  to_string(T).

A trait definition establishes a unit of shared bahavior. We can ask questions like “Does this type implement that trait?” And thus is akin to a single-arity Prolog predicate. Using Prolog conventions we have the to_string/1 predicate that declares its parameter an implementor of the ToString trait.We can provide a trait implementation for ground types. Shown in are the implementations for i32 and char. These implementations declare facts. A fact that these types satisfy the to_string predicate.With polymorphism we can chain trait implementations, such as the type-parameterized implementation for Vec<T>. These implementations form a rule. In order for the rule to be proven, several additional body predicates need to be satisfied. These predicates are the clauses that come after Rust’s where keyword, or after Prolog’s :- in the rule body.Callling our print_ln function with a vector of floating-point numbers created a trait bound, Vec<f32>: ToString. Non-parameterized types are converted to atoms in the logic model. It is then the compiler’s job to resolve the ToString implementation for the instantiated type T. In logic programming we can phrase this bound as a query, ?- to_string(vec(f32)), interpreting this query is equivalent to to resolving the trait implementation. The funny ?- indicates that the clause is a question, not a statement.

We take the definition of logic program computation from Sterling and Shapiro1994: computation progresses via goal reduction. At each stage there is a conjunction of goals to be proved, this is called the resolvent. The interpreter will choose a goal from the resolvent and a clause from the program environment such that the clause head unifies with the goal. (A clause is either a fact or a rule.) The computation continues by replacing the resolvent with the clause’s body. When picking a goal and clause, we constrain the interpreter to choose left-to-right and top-to-bottom, respectively. After successfully proving a goal in the conjunction the interpreter continues to the next. After failing to prove a goal the interpreter backtracks to the last point of choice, where a clause was picked from the environment, and chooses the next clause if one is available. Tracing the execution of the described interpreter constructs a proof tree. Each goal has a set of candidate clauses from which the interpreter can choose to perform goal reduction. Reducing a goal with a rule clause introduces a conjunction of subgoals that must be proven. If a goal fails, the interpreter can backtrack and retry by reducing the goal with a different clause. This was quite a bit of technical information, but the visualization clarifies the proof tree structure.

Tracing the execution of the simple program using ToString, we get the proof tree shown in , goals connected by a dashed line represent an Or relationship. At least one child in an Or relationship must hold for the parent to be proven. Goals connected with a solid line form an And relationship. All child goals must be proven for their parent to be proven. This type of proof tree is commonly referred to as an And–Or tree. Each level in the tree is either a conjunction: all child goals must be proven, or a disjunction: at least one child goal must be proven.

to_string(i32);
to_string(char);

to_string(vec(T)) :-
  to_string(T);

?- to_string(vec(f32)).

flowchart TD
  classDef invisible display:none
  C["to_string(f32)"]
  B["to_string(vec(f32)) :- to_string(f32)"]
  A["?- to_string(vec(f32))"]
  D["No"]
  C ~~~ D
  A ~~~ B
  B ~~~ C
  class D,B,C invisible

The execution of this program was as follows. The start of the search process is the root goal. This is where the Rust trait solver asks “Does Vec<f32> implement ToString?”

to_string(i32);
to_string(char);

to_string(vec(T)) :-
    to_string(T);

?- to_string(vec(f32)).

flowchart TD
  classDef invisible display:none
  C["to_string(f32)"]
  B["to_string(vec(f32)) :- to_string(f32)"]
  A["?- to_string(vec(f32))"]
  D["No"]
  C ~~~ D
  A -.-> B
  B --> C
  class D invisible

The interpreter unifies the goal with the rule head from the program. Unifying to_string(vec(T)) = to_string(vec(f32)) results in the constraint T = f32. The current goal is reduced to the body of the rule, to_string(f32). In this case there is only one goal of the rule body, if there were many, they would be conjunctive. These conjunctive nodes are siblings in the proof tree and they form an And relationship with their parent. This means that for the parent goal to be proven, all children must be proven.

to_string(i32);
to_string(char);

to_string(vec(T)) :-
  to_string(T);

?- to_string(vec(f32)).

flowchart TD
  classDef invisible display:none
  C["to_string(f32)"]
  B["to_string(vec(f32)) :- to_string(f32)"]
  A["?- to_string(vec(f32))"]
  D["No"]
  C --> D
  A -.-> B
  B --> C

The now current goal, to_string(f32), fails to unify with any clause in the program. Therefore this goal cannot be proven. There are no other rules the interpreter can backtrack to. Therefore, the root goal, to_string(vec(f32)) cannot be proven. It’s then said that the trait bound Vec<f32>: ToString is not satisfied.

Now that terminology is out of the way and we’ve seen a simple example, it’s time to start looking at the proof tree for the Axum trait error. The resulting proof tree for the simple ToString trait was more of a proof stick, no backtracking occurred. Let us direct our attention to the running example with Axum, introduced in , where we will see some branching.

Type-checking a Web Server

fn_once([], _).
fn_once([_|_], _).

from_request_parts(parts(_)).
from_request(bytes).
from_request(string).

future(promise(O), O).
into_response(string).

handler(fn_once([T1], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request(T1).

handler(fn_once([T1, T2], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request_parts(T1),
    from_request(T2).

?- handler(fn_once([string, bytes]), promise(string)).

flowchart LR
  classDef invisible display:none
  C["No"]
  B["handler(fn_once([T1], Fut)) :- ..."]
  A["?- handler(<br/>  fn_once([string, bytes]),<br/>  promise(string)<br/>)."]
  G["from_request_parts(string)"]
  F["into_response(string)"]
  E["future(promise(string), string)"]
  D["handler(fn_once([T1, T2], Fut)) :- ..."]
  K["Yes"]
  J["Yes"]
  I["from_request(bytes)"]
  H["No"]
  D ~~~ G
  D ~~~ E
  A ~~~ B
  E ~~~ J
  G ~~~ H
  D ~~~ F
  A ~~~ D
  D ~~~ I
  B ~~~ C
  F ~~~ K
  class H,I,J,K,D,E,F,G,B,C invisible

We start with the root goal, asking whether the type login implements Handler. In Rust, login has typeThe logic version of the Axum API uses the atom promise to represent something that implements the future trait. This is a bit over-simplified from the Rust Async model, but an unimportant detail for this example.

fn(String, Bytes) -> impl Future<Output = String>

fn_once([], _).
fn_once([_|_], _).

from_request_parts(parts(_)).
from_request(bytes).
from_request(string).

future(promise(O), O).
into_response(string).

handler(fn_once([T1], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request(T1).

handler(fn_once([T1, T2], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request_parts(T1),
    from_request(T2).

?- handler(fn_once([string, bytes]), promise(string)).

flowchart LR
  classDef invisible display:none
  C["No"]
  B["handler(fn_once([T1], Fut)) :- ..."]
  A["?- handler(<br/>  fn_once([string, bytes]),<br/>  promise(string)<br/>)."]
  G["from_request_parts(string)"]
  F["into_response(string)"]
  E["future(promise(string), string)"]
  D["handler(fn_once([T1, T2], Fut)) :- ..."]
  K["Yes"]
  J["Yes"]
  I["from_request(bytes)"]
  H["No"]
  D ~~~ G
  D ~~~ E
  A -.-> B
  E ~~~ J
  G ~~~ H
  D ~~~ F
  A ~~~ D
  D ~~~ I
  B --> C
  F ~~~ K
  class H,I,J,K,D,E,F,G invisible

Our interpreter chooses clauses top-to-bottom. The first rule handler(fn_once([T1], Fut)) is tried but automatically fails. We’ve said that the rule head needs to unify with the goal and in this case the arity of the goal and rule head functions differ—two vs one.

fn_once([], _).
fn_once([_|_], _).

from_request_parts(parts(_)).
from_request(bytes).
from_request(string).

future(promise(O), O).
into_response(string).

handler(fn_once([T1], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request(T1).

handler(fn_once([T1, T2], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request_parts(T1),
    from_request(T2).

?- handler(fn_once([string, bytes]), promise(string)).

flowchart LR
  classDef invisible display:none
  C["No"]
  B["handler(fn_once([T1], Fut)) :- ..."]
  A["?- handler(<br/>  fn_once([string, bytes]),<br/>  promise(string)<br/>)."]
  G["from_request_parts(string)"]
  F["into_response(string)"]
  E["future(promise(string), string)"]
  D["handler(fn_once([T1, T2], Fut)) :- ..."]
  K["Yes"]
  J["Yes"]
  I["from_request(bytes)"]
  H["No"]
  D --> G
  D --> E
  A -.-> B
  E ~~~ J
  G ~~~ H
  D --> F
  A -.-> D
  D --> I
  B --> C
  F ~~~ K
  class H,J,K invisible

Continuing its search the interpreter backtracks and tries to reduce the goal via a different clause, the second implementation rule for handler. The second clause head does unify with the current goal. Take note that these two rules form an Or relationship with the root goal. The first failed but the root goal may still be proven via the second clause. After the clause head unified, the goal is replaced by the clause body. The subgoals introduced in the reduction are a conjunction, forming an And relationship with the parent rule.

fn_once([], _).
fn_once([_|_], _).

from_request_parts(parts(_)).
from_request(bytes).
from_request(string).

future(promise(O), O).
into_response(string).

handler(fn_once([T1], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request(T1).

handler(fn_once([T1, T2], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request_parts(T1),
    from_request(T2).

?- handler(fn_once([string, bytes]), promise(string)).

flowchart LR
  classDef invisible display:none
  C["No"]
  B["handler(fn_once([T1], Fut)) :- ..."]
  A["?- handler(<br/>  fn_once([string, bytes]),<br/>  promise(string)<br/>)."]
  G["from_request_parts(string)"]
  F["into_response(string)"]
  E["future(promise(string), string)"]
  D["handler(fn_once([T1, T2], Fut)) :- ..."]
  K["Yes"]
  J["Yes"]
  I["from_request(bytes)"]
  H["No"]
  D --> G
  D --> E
  A -.-> B
  E --> J
  G ~~~ H
  D --> F
  A -.-> D
  D --> I
  B --> C
  F ~~~ K
  class H,K invisible

Working left-to-right, the goal future(promise(string), Res) needs to be proven as part of the conjunction. The interpreter unifies this with a program fact and the subgoal is said to be proven. The effect of this unification is the learned constraint, Res = string.

fn_once([], _).
fn_once([_|_], _).

from_request_parts(parts(_)).
from_request(bytes).
from_request(string).

future(promise(O), O).
into_response(string).

handler(fn_once([T1], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request(T1).

handler(fn_once([T1, T2], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request_parts(T1),
    from_request(T2).

?- handler(fn_once([string, bytes]), promise(string)).

flowchart LR
  classDef invisible display:none
  C["No"]
  B["handler(fn_once([T1], Fut)) :- ..."]
  A["?- handler(<br/>  fn_once([string, bytes]),<br/>  promise(string)<br/>)."]
  G["from_request_parts(string)"]
  F["into_response(string)"]
  E["future(promise(string), string)"]
  D["handler(fn_once([T1, T2], Fut)) :- ..."]
  K["Yes"]
  J["Yes"]
  I["from_request(bytes)"]
  H["No"]
  D --> G
  D --> E
  A -.-> B
  E --> J
  G ~~~ H
  D --> F
  A -.-> D
  D --> I
  B --> C
  F --> K
  class H invisible

Continuing in the interpretation we now have to prove the subgoal into_response(string). One again a fact from the program unifies with the goal and it is said to be proven. IntoResponse is the set of types the Axum API knows how to convert into an HTTP response.

fn_once([], _).
fn_once([_|_], _).

from_request_parts(parts(_)).
from_request(bytes).
from_request(string).

future(promise(O), O).
into_response(string).

handler(fn_once([T1], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request(T1).

handler(fn_once([T1, T2], Fut)) :-
    future(Fut, Res),
    into_response(Res),
    from_request_parts(T1),
    from_request(T2).

?- handler(fn_once([string, bytes]), promise(string)).

flowchart LR
  classDef invisible display:none
  C["No"]
  B["handler(fn_once([T1], Fut)) :- ..."]
  A["?- handler(<br/>  fn_once([string, bytes]),<br/>  promise(string)<br/>)."]
  G["from_request_parts(string)"]
  F["into_response(string)"]
  E["future(promise(string), string)"]
  D["handler(fn_once([T1, T2], Fut)) :- ..."]
  K["Yes"]
  J["Yes"]
  I["from_request(bytes)"]
  H["No"]
  D --> G
  D --> E
  A -.-> B
  E --> J
  G --> H
  D --> F
  A -.-> D
  D --> I
  B --> C
  F --> K

The first parameter type of the function login, String must implement FromRequestParts. The goal, from_request_parts(string), does not unify with any program clause. Therefore, the goal fails. At this point, the interpreter has exhausted the disjunction of clause rules and can no longer backtrack. The root goal can therefore also not be proven and execution halts.

Diagnosing Errors

Each of the running example programs was translated into an equivalent logic program, and the queries were traced to build proof trees. Both trees in and failed, and the compiler must turn this proof tree into a diagnostic message. We can partially formalize this final step in the compiler as a function, diagnose, that takes a tree as input and returns the problematic tree node.

diagnose :: ProofTree -> Node

The diagnose function is reductive. It takes the large data of a proof tree and chooses a small piece to show developers. There is a tension in forming error diagnosis as a reduction. Diagnostics want to be as helpful as possible, reflect on our criteria for a good diagnostic: it must determine the specific root cause and includes full provenance of the failure. Shown in are the two failing proof trees for the good and poor diagnostics.

The ToString examples produces a simple tree. There only exists a single failing node! In this case the reduction is straightforward, by reducing the tree to its single failing node, to_string(f32), no information has been lost. The specific root cause is the failing node and the provenance is generated by traversing the tree upwards, from failing node to root. The complex tree produced by the Axum Handler example is not as straightforward. Here the reduction must choose between two failing nodes, however, choosing either of the nodes forgets the information of the other failed branch. Compiler diagnostics are conservative, so rather than reduce the tree to a failed node the tree is reduced to the least common ancestor of the failed nodes.

One’s initial intuition may be to simply improve reduction algorithm. This is equivalent to “making diagnostics better.” Indeed there are circumstances where type information may be able to eliminate certain failed branches, but the problem is still that of reduction.

This thesis proposes to change the fundamental problem of error diagnosis. We proposes an alternative function, ui, to the reductive diagnose:The type constructor Visualize is doing a lot of heavy lifting in this signature.

ui :: ProofTree -> Visualize ProofTree

No longer is error diagnosis a reduction problem. By changing the output type from Node to Visualize ProofTree, the problem is now an interface problem. We want to facilitate information extraction from the proof tree and allow developers to discover the root cause of an error, while preserving provenance. The benefit is that no information is lost; the root cause of an error is always available. The drawback, again, is that no information is lost. Proof trees are large and complex, and the designed interface should facilitate localizing the root cause with as few interactions as possible.