What does coherence mean?

Question

In the paper "Type classes: exploring the design space" by Simon Peyton Jones, Mark Jones and Erik Meijer, they define coherence informally as follows:

Every different valid typing derivation for a program leads to a resulting program that has the same dynamic semantics.

First of all, programs don't have types; expressions, variables and functions have types. So I guess I will interpret it as saying that each program fragment (expression, variable or function) must have a unique type derivation.

Then I wonder if Haskell (say Haskell2010) is really coherent? E.g. the expression \x -> x can be given the type a -> a, but also Int -> Int. Is does that mean that coherence is broken? I can think of two rebuttals:

1. Int -> Int is not a valid typing derivation, the term \x -> x gets the inferred type a -> a which is strictly more general than Int -> Int.

2. The dynamic semantics are the same in both cases, it is just that the type Int -> Int is less general and will be rejected statically in some contexts.

Which of these are true? Are there other counterarguments?

Now let's consider type classes, because coherence is often used in that context.

There are several ways in which Haskell as implemented by GHC possibly breaks coherence. Obviously the IncoherentInstances extension and the related INCOHERENT pragma seem relevant. Orphan instances also come to mind.

But if point 1 above is true, then I would say that even these don't break coherence, because we could just say that the instance selected by GHC is the one true instance that should be chosen (and all the other type derivations are invalid), just like how the type inferred by GHC is the true type that has to be chosen. So point 1 is probably not true.

Then there are more innocent seeming extensions like overlapping instances via the OverlappingInstances extension or the Overlapping, Overlaps and Overlappable pragmas, but even the combination of MultiParamTypeClasses and FlexibleInstances can give rise to overlapping instances. E.g.

class A a b where
  aorb :: Either a b

instance A () b where
  aorb = Left ()

instance A a () where
  aorb = Right ()

x :: Either () ()
x = aorb

The FlexibleInstances and MultiParamTypeClasses extensions are included in GHC2021 so I would certainly hope that they don't break coherence. But I don't think point 1 above is true and point 2 doesn't seem to apply here because the dynamic semantics are really different.

I would also like to mention the defaulting system. Consider:

main = print (10 ^ 100)

By default GHC (and maybe Haskell2010?) will default to using Integer for both 10 and 100. So the result prints a one with a hundred zeroes. But if we now add a custom defaulting rule:

default (Int)

main = print (10 ^ 100)

Then both 10 and 100 default to the type Int and due to wrapping this prints only a single zero. So the expression 10 ^ 100 has different dynamic semantics in different context. Is that incoherent?

So my question is: is there a more formal or more detailed definition of coherence that can resolve the questions raised above?

Ivanna

Answer 1

Incoherence does not result from a lack of uniqueness of types. Take your example:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

class A a b where
  aorb :: Either a b

instance A () b where
  aorb = Left ()

instance A a () where
  aorb = Right ()

x :: Either () ()
x = aorb

There is no problem uniquely assigning types here. Specifically, the types/kinds of top-level identifiers defined in the module are:

A :: Type -> Type -> Constraint
aorb :: (A a b) => Either a b
x :: Either () ()

If you are concerned about the type of the expression aorb used on the right hand side of x = aorb, it's unambiguously Either () (). You can use a type wildcard x = (aorb :: _) to verify this:

error: Found type wildcard '_' standing for 'Either () ()'

The reason this program is incoherent (and the reason GHC rejects it) is that multiple type DERIVATIONS for the type of x :: Either () () are possible. In particular, one derivation uses the instance A () b, while the other uses the instance A a (). I emphasize: both derivations lead to the same typing of the top-level identifier x :: Either () () and the same (static) typing of the expression aorb in x = aorb (namely Either () ()), but they lead to a different term-level definition of aorb being used in the code generated for x. That is, x will exhibit different dynamic semantics (term-level computation) with the same static semantics (type-level computation) depending on which of the two valid typing derivations is used.

This is the essence of incoherence.

So, getting back to your original questions...

You should think of the "typing derivation for a program" as being the entirety of the type-checking process, not just the final types assigned to program fragments. Formally, the "typing" of a program (i.e., the types of all its constituent parts) is a theorem that must be proved to accept a program as well typed. The "typing derivation" of a program is the proof of that theorem. The static semantics of the program are determined by the statment of the theorem. The dynamic semantics are determined in part by the proof of that theorem. If two valid derivations (proofs) lead to the same static typing (theorem) but different dynamic semantics, the program is incoherent.

The expression \x -> x may be typed as a -> a or Int -> Int, depending on context, but the fact that multiple typings are possible is unrelated to incoherence. In fact, \x -> x is always coherent, because the same "proof" (typing derivation) can be used to prove the type a -> a or Int -> Int, depending on context. Actually, as pointed out in the comments, this isn't quite right: the proof/derivation is a little different for different types, but the proof/derivation always leads to the same dynamic semantics. That is, dynamic semantics of the term level definition \x -> x are always "take an argument and return it", regardless of how \x -> x is typed.

The extensions FlexibleInstances and MultiParamTypeClasses can introduce incoherence. In fact, your example above is rejected because it is incoherent. Overlapping instances provide a mechanism to regain coherence, by prioritizing some derivations over others, but they don't work here. The only way to get your example to compile is using incoherent instances.

Defaulting, too, is unrelated to coherence. With the default defaulting, the program:

main = print (10 ^ 100)

has a typing that assigns type Integer to 10 and 100. With different defaulting, the same program has a typing that assigns type Int to 10 and 100. In each case, the static typing of the program is different (i.e., the expression 10 ^ 100 has static type Integer in the first case and Int in the second), and programs with different static typing (different type-level theorems) are different programs, so they're allowed to have different dynamic semantics (different term-level proofs).

Gooden

So to summarize: coherence is about type checking derivations (which always results in a predetermined type) and not about type inference derivations (which could result in different types; are these even called derivations?). That answers my questions, thanks! – Ivanna

@Ivanna Re: your terminology question, the way I would say it is: Type inference is the process of searching for a type that has a derivation. – Latex

This is a great answer, and I have just one nitpick: I wouldn't call the obvious derivations for \x -> x :: a -> a and \x -> x :: Int -> Int the same -- at least, not if we think of \x -> x :: a -> a as actually being shorthand for \x -> x :: forall a. a -> a, which requires a generalization step that's not needed for Int -> Int. I'd even argue that the derivations for \x -> x :: Bool -> Bool and \x -> x :: Int -> Int are different, because the lambda typing rule puts different things in the environment in the two derivations. – Latex

@DanielWagner, yes I think you're right. I was actually thinking of \x -> x as the term-level "proof" of both the theorem forall a. a -> a and Int -> Int. But, this isn't precisely correct. As you rightly point out, the term proves the theorem through a chain of rules, and two syntactically identical terms that prove their theorems through different chains are rightly considered different derivations/proofs. In particular, x = aorb is incoherent precisely because the same term gives rise to two different derivations/proofs. – Gooden

I made a slight change to try to clarify. – Gooden