Inside 245-5D

Existential Pontification and Generalized Abstract Digressions

Type classes: confluence, coherence and global uniqueness

Today, I'd like to talk about some of the core design principles behind type classes, a wildly successful feature in Haskell. The discussion here is closely motivated by the work we are doing at MSRC to support type classes in Backpack. While I was doing background reading, I was flummoxed to discover widespread misuse of the terms "confluence" and "coherence" with respect to type classes. So in this blog post, I want to settle the distinction, and propose a new term, "global uniqueness of instances" for the property which people have been colloquially referred to as confluence and coherence.

Let's start with the definitions of the two terms. Confluence is a property that comes from term-rewriting: a set of instances is confluent if, no matter what order constraint solving is performed, GHC will terminate with a canonical set of constraints that must be satisfied for any given use of a type class. In other words, confluence says that we won't conclude that a program doesn't type check just because we swapped in a different constraint solving algorithm.

Confluence's closely related twin is coherence (defined in the paper "Type classes: exploring the design space"). This property states that every different valid typing derivation of a program leads to a resulting program that has the same dynamic semantics. Why could differing typing derivations result in different dynamic semantics? The answer is that context reduction, which picks out type class instances, elaborates into concrete choices of dictionaries in the generated code. Confluence is a prerequisite for coherence, since one can hardly talk about the dynamic semantics of a program that doesn't type check.

So, what is it that people often refer to when they compa

11 Responses to “Type classes: confluence, coherence and global uniqueness”

  1. Mikhail Glushenkov says:

    Thanks, a very informative post. But note that a variant of this problem crops up even when global uniqueness of instances holds:

    Perhaps we should be talking about “global instance coherence”?

  2. Aaron Levin says:

    I’ve even wondering about this for a while, coming to Haskell from Scala. Thanks!

    Can expand on what you meant by this: “Furthermore, the types of ins and ins’ discharge type class resolution”?

    I am very surprised GHC didn’t throw an error in that example!


  3. Aaron Levin says:

    (Sorry about typos, on mobile)

  4. Aaron: Because the type of ins does not have a type class constraint in it, it means that any use of type classes was resolved at the definition site, and that the user of the library did not need to do any type class resolution.

  5. Dominique Devriese says:

    @Mikhail Glushenkov: I don’t understand why you say that global uniqueness holds for your example. It has two different instances for constraint Ord (T U MB MC), no?

  6. Mikhail Glushenkov says:

    @Dominique Devriese

    Hmm, now after looking again at Edward’s post, I think you’re right. The point of that example is that implementing a global instance uniqueness check in GHC is not as easy as just emitting a symbol for each instance declaration in the program and then relying on linker to produce an error.

  7. Steven Shaw says:

    When I compile and run your second example, it doesn’t (seem to) terminate!
    GHC 7.8.3 on Mac 10.10.1

    Is this the last word on global uniqueness of instances in GHC? I had perhaps misunderstood that Haskell guaranteed it.

  8. Steven: So it goes! Perhaps the set implementation changed so that when the invariant is violated it loops. In any case it’s just another way things break when you have inconsistent instances.

    I wouldn’t call this the last word on global uniqueness; if we could have GHC check the instance easily we would, but we don’t because this situation is fairly rare and fixing this properly would penalize normal compilation times.

  9. Anonymous says:

    I agree that this kind of global instances is nonmodular and has other problem.

    In the example given, my opinion is that Haskell ought to allow to define a datatype (or newtype) to depend on a constant, therefore (Set x) depends on (Ord x), and specifying the type (Set U) in D.hs is an error because it is ambiguous which type you mean; (Set U) is going to be one type in B.hs and another type in C.hs. Even if you do specify, the ins and ins’ functions then aren’t composable because it is a type mismatch.

    Another problem with these global instances is that some packages define instances that are wrong (of: Alternative IO, MonadPlus IO, MonadTrans Free, etc) and then you cannot use the correct one!!!

  10. AntC says:

    Thanks Edward, sorry to be late to the party but somebody’s just linked to this piece. I was indeed aware that Haskell allows you to declare overlapping instances (even without the `Overlapping/Incoherent` flags or pragmas), but doesn’t warn you unless you try to use a function at the overlap. (Contrast that dear old Hugs used to validate instances ‘eagerly’ at the instance decl. And Type Family instances also validate eagerly, as a matter of type safety.)

    There’s a sentence that’s ambiguous (last of the second section).

    > Languages with local type class instances such as Scala generally do not have this property, and this assumption is a very convenient one when building abstractions like sets.

    Does “this assumption” mean the assumption of local instances? I think not: I think you mean the assumption of global uniqueness of instances is very convenient.

    Not just convenient, but essential for the laws to work: `Eq` is a superclass of `Ord`. So having `Ord a => Set a` is supposed to deliver uniqueness of elements within the set. What we don’t want by using both `ins’` and `ins` to construct a set is a duplicate `X`. That would be a bag, not a set.

    I presume your demonstration was to show a repeated `X` is a Bad Thing/a _reductio ad absurdum_. (There’s somebody seems to think it was the desired result.)

  11. I think I am in agreement with you, but I have reworded the sentence in question to remove the ambiguity (as I see it!)