8
$\begingroup$

Suppose two separate files define decidability instances for a particular predicate in different ways. If I import both of these files, and attempt to run #eval to_bool ... to evaluate the predicate for a particular input, how does Lean decide which instance to use in the evaluation?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ This is like asking "suppose I am about to shoot myself in the foot. Which foot will it be?" Your mistake is to define the two decidability instances in the first place. We call this a diamond and they're to be avoided. The answer to your question is "it's completely random in practice". $\endgroup$
    – Kevin Buzzard
    Commented Feb 26, 2022 at 9:00
  • 2
    $\begingroup$ In programming language design we like to think that some of the blame goes to whoever designed the shotgun and handed it to the programmer. $\endgroup$
    – Andrej Bauer
    Commented Feb 26, 2022 at 9:34

1 Answer 1

Reset to default
5
$\begingroup$

Instances for Decidable are resolved in the same manner as instances for other type classes, which is determined by the finer details of Lean's type class resolution algorithm. This algorithm has undergone major changes from Lean 3 to Lean 4, so the exact answer will be different between versions.

In Lean 3, as Kevin notes in his comment, the type class algorithm has trouble with such clashes and projects like mathlib work very hard at eliminating them from their codebase. They call such situations diamonds, though as Eric Wieser once noted on the Zulip forums, they are more wedges than diamonds.

In Lean 4, the algorithm was substantially improved and can handle diamonds much better. However, while Lean has gotten better at selecting instances in such cases, diamonds can still pose problems, as two uses of a type class can still end up selecting different instances. This often produces counterintuitive results (e.g., 0 ≠ 0).

Lean 4's algorithm is novel enough that the developers wrote a paper on it entitled "Tabled Typeclass Resolution" (the preprint of which is available on arXiv here). I would advise reading that paper if you are interested in the nitty gritty details of how it works. Sadly, I don't know of a similar write-up for Lean 3's type class resolution. Thus, the best way to figure out how it selects instances may be to look at the source code.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ What you say 0 ≠ 0 you can't possibly mean that diamonds are a source of inconsistency, right? You are just saying that the first 0 and the second 0 don't resolve to the same thing, so it looks like 0 is not equal to itself, but it is not really. $\endgroup$
    – Jason Rute
    Commented Feb 27, 2022 at 2:49
  • 1
    $\begingroup$ Am I correct in my understanding of that paper (especially fig 1) that diamonds are considered fine and even desirable in Lean 4 as long as all the different resolution paths lead to the same instance? Is it strongly desired that the different instances are definitionally equal, or is provably equal fine in practice? $\endgroup$
    – Jason Rute
    Commented Feb 27, 2022 at 3:00
  • 1
    $\begingroup$ @JasonRute Note that Figure 1 in the paper is about class inheritance,, not instance resolution, which is a different but related matter. Diamonds/wedges in inheritance can have other problems not related to resolution (e.g., clashes between fields names of distinct parents). $\endgroup$
    – tydeu
    Commented Feb 27, 2022 at 9:43
  • 1
    $\begingroup$ @JasonRute As to your other points: You are right about the zeroes and have got the general idea right about diamonds/wedges in Lean 4. They can be useful (e.g., they are utilized heavily by the core library's monad classes), and the common ways to resolve them are by either ensuring that all paths lead to the same instance (e.g., with priorities or declaration order), by ensuring they are definitionally equal, and/or by carrying some proof they are propositionally equal. However, there are still some major caveats, so care is needed when introducing them. $\endgroup$
    – tydeu
    Commented Feb 27, 2022 at 9:55
  • 1
    $\begingroup$ In Lean 3/mathlib, diamonds are extremely widespread and we take care to ensure the competing instances are definitionally equal, when possible. I have a paper on the arXiv that goes into more detail, especially section 7 and 8. $\endgroup$
    – Anne Baanen
    Commented Feb 28, 2022 at 10:08

Not the answer you're looking for? Browse other questions tagged or ask your own question.