Labelled preorders and implicit coercions › 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.