Allow Typeclasses to Declare Themselves Coherent

6 min read Original article ↗

Motivation

Unlike Haskell, Scala allows multiple implicit instances of a type. This makes implicits cover a lot more use cases. Besides type classes, implicits can also express

  • capabilities
  • configurations, which may be locally overridden
  • contexts in their full generality

When used for implementing typeclasses, implicits support different implementations of a type class in different modules. For instance, Boolean could implement Monoid with true and & in one part of a program and with false and | in another.

By contrast, Haskell's type classes have a coherence requirement which states that a type can implement a type class only in one way anywhere in a program. Coherence restricts what one can do with type classes. It feels a bit anti-modular since it establishes a condition for "a whole program" (in Scala or Java one would not even know what that is!). But it also solves two problems of Scala's unrestricted use of implicits.

The first problem is that one can accidentally mix two different implicit implementations where this is non-sensical. The classic example is a priority queue which requires an Ordered element type. If one declares priority queue like this:

class PriorityQueue[T: Ordered] { 
   ...
   def union(other: PriorityQueue[T]): PriorityQueue[T]
}

there's no way to guarantee that the two queues in a union operation agree on the ordering of type T. This can lead to nonsensical results. I believe this is a bit of a red herring however, as it is perfectly possible to design data structures that do not suffer from that problem by using some nesting (or functorizing, to borrow some ML terminology). For priority queues, Chris Okasaki's scads is a nice solution, which generalizes readily. In essence, all that's needed is to move the type parameter T one level further out:

class PriorityQueues[T: Ordered] {
  class Queue {
    ...
    def union(other: Queue): Queue
  }
}

So far, so good. But there's also a second problem which is in a sense the dual of the first. The first problem was "how do we prevent some programs from compiling when implementations are not coherent"? (i.e. we have multiple implementations of the same type class). The second problem is "how do we get some programs to compile when implementations are coherent"? In Scala, implicit resolution may lead to ambiguities, which are compile-time errors. But in a coherent world, ambiguities do not matter: picking any one of multiple applicable alternatives would give the same observable result. So if we know that all implementations of some type are coherent, we could suppress all ambiguity errors related to implicit searches of that type.

This is a real issue in practice, which mars attempts to implement in Scala typeclass hierarchies that are standard in Haskell. #2029 is a good starting point to explore the issue. Here's a somewhat more figurative explanation of the problem: Say you want to model capabilities representing driving permits as implicit values. There's a basic capability "has drivers license", call it DL. There are two more powerful capabilities "has truck driver's license" (TL) and "has cab license" (CL). These would be modelled as subtypes of the "drivers license" type. Now, take a function that requires the capabilities to drive a truck and to drive a cab, i.e. it takes two implicit parameters of type TL and CL. The body of the function needs at some point the capability of driving a car (DL). In the real world, this would be no problem since either of the function's capabilities TL and CL imply the capability DL. But in current Scala, you'd get an ambiguity, precisely because both implicit parameters of types TL and CL match the required type DL. In actual Scala code, this is expressed as follows:

trait DL
trait TL extends DL
trait CL extends DL

object Driving {
  def drive(implicit dl: DL) = ()
  def f(implicit tl: TL, cl: CL) = drive
}

Compiling this results in an ambiguity error:

-- Error: coherent.scala -------------------------------------------------------
33 |  def f(implicit tl: TL, cl: CL) = drive
   |                                        ^
   |ambiguous implicits: both value tl and value cl match type DL of parameter dl of method drive in object Driving

#2029 and @adelbertc's note contain discussions of possible workarounds. One workaround uses aggregation instead of subtyping. The other tries to bundle competing implicit parameters in a single implicit in order to avoid ambiguities. Neither approach feels both simple and scalable in a modular fashion.

Proposal

The proposal is to introduce a new marker trait scala.typeclass.Coherent.

package scala.typeclass
trait Coherent

If a type T extends directly or indirectly the Coherent trait, implicit searches for instances of type T will never issue ambiguity errors. Instead, if there are several implicit values of type T (where no value is more specific than any other) an arbitrary value among them will be chosen.

For instance, the Driving example above can be made to compile by changing the definition of DL to

trait CanDrive extends scala.typeclass.Coherent

Soundness

The rule for dealing with coherence makes some implicit selections unspecified. A global coherence condition is needed to ensure that such underspecifications cannot lead to undetermined behavior of a program as its whole. Essentially, we need to ensure that if there is more than one implicit value implementing a coherent type T, all such values are indistinguishable from each other. (In)distinguishability depends on the operations performed by the program on the implicit values. For instance, if the program compares implicit values using reference equality (eq), it can always distinguish them. One good rule to follow then is to avoid calling eq, as well as all other operations defined in AnyRef on values of coherent types. Furthermore, one needs to also ensure that all members of a coherent type are implemented in the same way in all implicit instances of that type.

It's conceivable that sufficient coherence conditions can be established and checked by a tool on a project-wide basis. This is left for future exploration, however. The present proposal defers to the programmer to check that coherence conditions are met.

Mixing coherent and normal abstractions

Sometimes one has conflicting requirements whether a type should be coherent or not. Coherency avoids ambiguity errors but it also prohibits possibly useful alternative implementations of a type. Fortunately, there's a way to have your cake and eat it too: One can use two types - a non-coherent supertype together with a coherent subtype.

For instance one could have a standard Monoid trait that admits multiple implementations:

package kernel
trait Monoid[T] {
   def empty: T
   def combine(x: T, y: T): Monoid[T]
}

One can then declare a coherent subtrait:

object Canonical {
   trait Monoid[T] extends kernel.Monoid[T] with Coherent
}

One could also several coherency domains by using a class instead of an object for Canonical and instantiating that class for each domain.

Alternatives

@djspiewak has proposed a different approach to coherence based on parameterizing implicit definitions with coherency domains. #2029 contains a discussion of this approach in relation to the present proposal.

Implementation Status

The proposal is implemented in #2046.