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.