From 599b0f6bdfe788ba3436d6f0b517914b0cfeddf2 Mon Sep 17 00:00:00 2001 From: gavinleroy Date: Tue, 27 Aug 2024 16:44:49 -0400 Subject: [PATCH] Small tweaks --- book/src/trait-debugging-101.md | 18 +++++++++--------- book/src/typestate.md | 4 +++- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/book/src/trait-debugging-101.md b/book/src/trait-debugging-101.md index cfe277a..e367420 100644 --- a/book/src/trait-debugging-101.md +++ b/book/src/trait-debugging-101.md @@ -77,8 +77,6 @@ The steps to respond to `Ty: Trait` proceed as follows. if `T` and `Ty` *unify*, proceed, otherwise respond no. -2. For each `Constrint_i`, restart the process with `Constrint_i` as the question. Respond with *yes* if all constraint responses are *yes*. - ```admonish note You may not know what we mean with "if they unify," so let's go over some examples. Two types unify in the trait solver if we can instantiate type variables such that they are equivalent. @@ -88,7 +86,9 @@ The steps to respond to `Ty: Trait` proceed as follows. - `Vec` and `Vec` unify if `U = T` ``` -2. Respond with *yes* if exactly one impl block responded with *yes*. +2. For each `Constrint_i`, restart the process with `Constrint_i` as the question. Respond with *yes* if all constraint responses are *yes*. + +3. Respond with *yes* if exactly one impl block responded with *yes*. Notice that these steps are recursive. When checking a where clause constraint the trait solver calls itself. The prosaic version is a bit nebulous, let's consider the diagramatic version instead. Consider the `Comparable` trait, we shall extend the previous program with one more impl block. @@ -148,9 +148,9 @@ graph TD; linkStyle 3 stroke:green, stroke-width:4px ``` -Dotted lines represent an **Or** relationship between parent and child. That is, exactly one of the child blocks needs to respond with 'yes.' We see these lines coming from the root question and extending to the impl blocks. Impl blocks always form an Or relationship with their parents. This models step (3) in the listed algorithm because one of the impl blocks must match, no more and no fewer. +Dotted lines represent an **Or** relationship between parent and child. That is, exactly one of the child blocks needs to respond with 'yes.' We see these lines coming from the root question and extending to the impl blocks. Impl blocks always form an Or relationship with their parents. This models step 3 in the listed algorithm because one of the impl blocks must match, no more and no fewer. -Solid lines represent **And** relationships between parent and child. That is, every one of the child blocks needs to respond with "yes." We see these lines coming from impl blocks and extending to the constraints. Constraints always form an And relationship with their parent impl block. Or rather, all constraints in a where clause must hold. +Solid lines represent **And** relationships between parent and child. That is, every one of the child blocks needs to respond with 'yes.' We see these lines coming from impl blocks and extending to the constraints. Constraints always form an And relationship with their parent impl block. Or rather, all constraints in a where clause must hold. ```admonish faq **Why does the trait solver check the impl block for `T` when there exists one directly for `Year`?** @@ -158,7 +158,7 @@ Solid lines represent **And** relationships between parent and child. That is, e The trait solver must consider all potentially matching impl blocks. Because `T` unifies with `Year`, the trait solver must check this block as well. Remember, if multiple impls work then this *is also* an error: ambiguous trait usage. Exactly one impl block must match for there to be a success. ``` -A neat pattern to observe is that a question always has a impl block as a child, with a dotted line. We can never have two questions in a row; you shouldn't answer a question with a question! Impl blocks always have a question as a child, with a solid line. If you follow a specific path in the tree the pattern of relationships will be "Or, And, Or, And, Or, And, …" +A neat pattern to observe is that a question always has an impl block as a child, with a dotted line. We can never have two questions in a row; you shouldn't answer a question with a question! Impl blocks always have a question as a child, with a solid line. If you follow a specific path in the tree the pattern of relationships will be "Or, And, Or, And, Or, And, …" The tree diagram above actually has a name, it's called the *search tree*. Search trees represent the execution of the trait solver! Just as you may have traced your own programs to debug strange behavior, we can trace the trait solver to help us understand why a particular outcome occurred. Search trees are the core data structure used in the Argus trait debugger, let's size up to a real example and see how we can use Argus to do some trait debugging. @@ -194,7 +194,7 @@ The above diagnostic, in a long-winded way, tells us that the function `login` d Going forward we will write `{login}` to abbreviate the type of `login`, `fn(LoginAttempt) -> bool`, which is far too verbose to repeat over and over. ``` -Fortunately, Argus is coming to the rescue! +When the compiler diagnostic says "trait `Bleh` is not implemented for type `Blah`", that's a great opportunity to use Argus.