Labelled preorders and implicit coercions › Approaches to the diamond problem(s) in existing systems [01HE]

Here I outline some (but not all) existing approaches to dealing with implicit coercions, multiple inheritance, and the various diamond problems.

1. Coherent type classes in Haskell [01HF]

Haskell employs a syntactic condition to ensure that type classes instances do not overlap, leading to a global coherence property. Practice in the Haskell community has shown that it is possible (but painful) to develop coherent hierarchies. Many advanced libraries will activate a language extension to allow overlapping instances, which renders the hierarchy incoherent.

2. Fast but incoherent type classes in Lean [01HG]

Type class hierarchies arising in mathematics tend to be unavoidably incoherent; therefore, systems like Lean implement a backtracking type class resolver and are therefore confronted with the second diamond problem above. The Lean team have discovered an algorithm that they call Tabled Typeclass Resolution that mitigates the exponential blow-up using ideas from logic programming.

The state of affairs for Lean is, then, that type class resolution is pretty fast but the actual resolution of coercions is in theory non-deterministic; in reality, it does the same thing every time (so far as I know), but there is no guarantee about which coercions it is choosing.

3. Coherent locale hierarchies in Isabelle [01HH]

Locales provide a coherent way to organise mathematical hierarchies. The problems that lead type class hierarchies to become incoherent do not seem to apply to locale hierarchies, I think, because the resolution of the locale’s operations is name-based rather than component-based. (I am not completely certain that this is the full story, but it seems like it is part of the story.)

One way to think about locales and the reason they can remain coherent is by analogy with Haskell’s newtype trick, which Haskell programmers use liberally to maintain coherence, but taken to its logical conclusion. Instead of generating a fresh copy of a type in order to indicate its intended role in the type class hierarchy, Isabelle doesn’t hang identity on the type at all and instead just starts with the name that carries intentional force.

The coherence of the locale hierarchy in Isabelle is checked when activating a locale as a local theory. Here, an algorithm called “roundup” reaches through the entire locale inheritance graph and brings all the needful operations into scope, and if there is a clash (two names pointing to different things), this results in an error. Such a clash always corresponds to a failure of coherence, and conversely, failures of coherence will always lead to such clashes.

4. Coherent coercions in Rocq [01HI]

Rocq has a coercion mechanism, which checks coherence and warns users when they are installing incoherent coercions. Coercions are most used in the world of Mathematical Components in combination with the canonical structures feature, which simulates type-class like features using something like unification hints (to my knowledge).

The algorithm used in Rocq was created by Kazuhiko Sakaguchi and described in the PhD thesis Refinement and extension of mathematical structures in proof assistants based on dependent type theory. The idea here is to maintain the reflexive-transitive closure (path category) of the coercion graph at all times; when inserting a new coercion, you check a generating class of diamonds for coherence and then add all the induced paths. Coherence then ensures that the path category is a preorder, with a functorial embedding into the syntactic category of the language under consideration.

References

    Reference. Refinement and extension of mathematical structures in proof assistants based on dependent type theory [sakaguchi-2023]

    • September, 2023
    • Kazuhiko Sakaguchi
    • PhD Thesis, Graduate School of Systems and Information Engineering, University of Tsukuba

    Reference. Tabled Typeclass Resolution [selsam-ullrich-demoura-2020]

    Typeclasses provide an elegant and effective way of managing ad-hoc polymorphism in both programming languages and interactive proof assistants. However, the increasingly sophisticated uses of typeclasses within proof assistants, especially within Lean’s burgeoning mathematics library, mathlib, have elevated once-theoretical limitations of existing typeclass resolution procedures into major impediments to ongoing progress. The two most devastating limitations of existing procedures are exponential running times in the presence of diamonds and divergence in the presence of cycles. We present a new procedure, tabled typeclass resolution, that solves both problems by tabling, which is a generalization of memoizing originally introduced to address similar limitations of early logic programming systems. We have implemented our procedure for the upcoming version (v4) of Lean, and have confirmed empirically that our implementation is exponentially faster than existing systems in the presence of diamonds. Although tabling is notoriously difficult to implement, our procedure is notably lightweight and could easily be implemented in other systems. We hope our new procedure facilitates even more sophisticated uses of typeclasses in both software development and interactive theorem proving.

    Context

      Labelled preorders and implicit coercions [01HB]

      Project Pterodactyl aims to support coherent algebraic hierarchies with multiple inheritance as well as user-defined edges. As I mentioned in my HoTTEST talk, there are a few points worth mentioning here in regard to the so-called “diamond problem”.

      What is the diamond problem? [01HD]

      The first thing to get out of the way is that the phrase “diamond problem” means different things to different people. There are actually two different diamond problems that arise when building systems that support implicit coercion; these two problems are actually mutually exclusive, in the sense that you can have only one version of the diamond problem at once.

      1. There is the coherence problem, which concerns ensuring that diamonds (and loops) in the coercion graph commute. A system in which all diamonds and loops commute is called coherent. In a coherent system, backtracking is never required and so the resolution of coercions can be extremely efficient. This is the “diamond problem” for Theory B computer scientists.
      2. In an incoherent system, resolution of coercions must traverse all possible paths from the source to the target, and the presence of diamonds and loops in the graph can cause an exponential blowup for the naïve backtracking algorithm. This is the “diamond problem” for Theory A computer scientists.

      Indeed, if your system is coherent then no backtracking is required; but you must find a way to maintain the coherence invariant. On the other hand, if you have an intentionally incoherent system, then you do have to deal with the exponential blowup, but you don’t have to check coherence because you don‘t care about coherence. This is the sense in which the two problems are mutually exclusive.

      Approaches to the diamond problem(s) in existing systems [01HE]

      Here I outline some (but not all) existing approaches to dealing with implicit coercions, multiple inheritance, and the various diamond problems.

      Coherent type classes in Haskell [01HF]

      Haskell employs a syntactic condition to ensure that type classes instances do not overlap, leading to a global coherence property. Practice in the Haskell community has shown that it is possible (but painful) to develop coherent hierarchies. Many advanced libraries will activate a language extension to allow overlapping instances, which renders the hierarchy incoherent.

      Fast but incoherent type classes in Lean [01HG]

      Type class hierarchies arising in mathematics tend to be unavoidably incoherent; therefore, systems like Lean implement a backtracking type class resolver and are therefore confronted with the second diamond problem above. The Lean team have discovered an algorithm that they call Tabled Typeclass Resolution that mitigates the exponential blow-up using ideas from logic programming.

      The state of affairs for Lean is, then, that type class resolution is pretty fast but the actual resolution of coercions is in theory non-deterministic; in reality, it does the same thing every time (so far as I know), but there is no guarantee about which coercions it is choosing.

      Coherent locale hierarchies in Isabelle [01HH]

      Locales provide a coherent way to organise mathematical hierarchies. The problems that lead type class hierarchies to become incoherent do not seem to apply to locale hierarchies, I think, because the resolution of the locale’s operations is name-based rather than component-based. (I am not completely certain that this is the full story, but it seems like it is part of the story.)

      One way to think about locales and the reason they can remain coherent is by analogy with Haskell’s newtype trick, which Haskell programmers use liberally to maintain coherence, but taken to its logical conclusion. Instead of generating a fresh copy of a type in order to indicate its intended role in the type class hierarchy, Isabelle doesn’t hang identity on the type at all and instead just starts with the name that carries intentional force.

      The coherence of the locale hierarchy in Isabelle is checked when activating a locale as a local theory. Here, an algorithm called “roundup” reaches through the entire locale inheritance graph and brings all the needful operations into scope, and if there is a clash (two names pointing to different things), this results in an error. Such a clash always corresponds to a failure of coherence, and conversely, failures of coherence will always lead to such clashes.

      Coherent coercions in Rocq [01HI]

      Rocq has a coercion mechanism, which checks coherence and warns users when they are installing incoherent coercions. Coercions are most used in the world of Mathematical Components in combination with the canonical structures feature, which simulates type-class like features using something like unification hints (to my knowledge).

      The algorithm used in Rocq was created by Kazuhiko Sakaguchi and described in the PhD thesis Refinement and extension of mathematical structures in proof assistants based on dependent type theory. The idea here is to maintain the reflexive-transitive closure (path category) of the coercion graph at all times; when inserting a new coercion, you check a generating class of diamonds for coherence and then add all the induced paths. Coherence then ensures that the path category is a preorder, with a functorial embedding into the syntactic category of the language under consideration.

      Evaluating: Isabelle‘s roundup algorithm vs. Rocq’s coercion graph [01HJ]

      I am ruling out incoherent hierarchies from the outset, because these lead to unpredicatable resolution. The two viable approaches seem therefore to be the one of Isabelle and the one of Rocq; I believe that the latter will work best for our needs, even if our goal is to enable an Isabelle-style user experience.

      The thing with Isabelle’s “roundup” algorithm is that it seems to rely heavily on the idea that the instances of a locale in scopes are fully top-level, so that you can walk through them and eagerly install all their operations into the appropriate scope. In this sense, Isabelle’s implementation of locales does not involve implicit coercion at all. In a dependent type theoretic setting, we must account for things like families of structures and ensuring that we can project components from these as well. For example, if we have a constant \(M \colon I \to \mathsf {Monoid}\), we will need to be able to call things like \((M~i).\mathsf {join}\) which would involve passing through the coercion to semigroups, etc. I am not sure how to capture something like that via a roundup-like algorithm.

      For this reason, I believe that the best foundation for Pterodactyl’s handling of algebraic hierarchies will be Sakaguchi’s labelled preorders as deployed in Rocq.

      A clean-room implementation of Sakaguchi’s labelled preorders [01HK]

      In order to learn how the algorithm works, I built a clean-room generic implementation in Swift of the labelled preorder structure following Sakaguchi’s algorithm. (Oh, did I mention I’m using Swift?)

      Our case will be a bit simpler than that of Rocq. In Rocq, coercions can be between arbitrary things, and therefore the vertices must include definitional equivalence classes of terms. That seems very tricky! We will be using a more restricted kind of coercion in Pterodactyl, where the vertices are only theory names. (We might later on also support coercions to sorts like those of types and functions, like Rocq does, which would not be difficult.)

      As a result, the only thing that we need to use expensive definitional equality checks for is the coercion paths themselves. It will indeed be pretty costly to install coercions, but resolving them will be very cheap: it is a single lookup in a hashtable by a totally discrete key. My code is available here.

      I am not certain that we will use literally this code (abstracting and modularising too early can be hazardous), but it’s a good start.