What kind of typeclass coherence should we support?

[odersky]

Scala does not have a global coherence requirement for its implicits.

2046 contains a discussion whether this should be changed and section 9 of #4153 contains another proposal to have local, instead of global coherence.

We should arrive at a decision what we want to do:

• no coherence (status quo)
• local coherence
• global coherence, unchecked
• global coherence, checked (but how?)

[DavidGregory084]

I don't think any discussion of coherence would be complete without a link to the Cochis paper, as even if we don't want to consider applying that algorithm the Related Work section is a good summary of the different approaches :smile:

[mdedetrich]

Not sure if this is possible, but I think having uncheck global coherence (as a default) and a keyword to specify that a certain typeclass requires coherence.

For some typeclasses you definitely wan't coherence, i.e. the principled typeclasses (stuff like Functor/Applicative). In this case you really do only want one coherent typeclass. On the other hand, typeclasses like Circe's Encoder/Decoder its entirely logical that you would have different implementations (in fact at work we have this because different services represent the same typeT in different ways and because of this we have different Encoder/Decoder because of this). Also don't really want to replicate the Haskell newtype boilerplate ceremony that they have to do here.

Not sure what the syntax of typeclasses is going to be, but something like this is what I would image

// default case, not coherent
typeclass Semigroup[A] {
  def combine(l: A)(r: A): A
}

vs

// coherent typeclasses, i.e. Haskell style
coherent typeclass Semigroup[A] {
  def combine(l: A)(r: A): A
}

Or something along these lines. Note that the above is for illustrative reasons, for SemiGroup you would always want a coherent typeclass. Ordering is another example of a typeclass where you may not want coherence.

[jesnor]

I wrote a blog post about a possible solution (with added compiler support) to global coherence which is optional on both the declaration and use sites. It could be a starting point for solution ideas.

[odersky]

Another critical design question for checked global coherence are orphan instances.

Haskell allows them, and there are good use cases for them since they reduce dependencies on library modules. The price to pay is that coherence errors might persist until link time. For Scala on the JVM with lazy loading this means that coherence errors might only be detected at runtime, and only in rare cases (say an exception path causes a new library to be loaded which causes a program crash due to a coherence error -- not what you want!)

Rust disallows them, it requires all instances to be defined "in the vicinity" of either the instance type or the implemented trait. What "in the vicinity" means is complicated and has evolved over the Rust releases.

[jesnor]

IMHO orphan instances should definitely be allowed, they are a useful design tool. I think they only pose a problem when only one unique type class instance is allowed (like in Haskell). My proposed solution linked above allows multiple instances to be defined, but adds extra type information which can be used to uniquely identify each one (or rather a group of semantically equivalent ones). In each use site one can then choose to either use a specific instance or any instance implementing the type class interface.

[Blaisorblade]

Any (known) use case for orphan instances for coherent typeclasses? If not, I'd allow orphans for coherent typeclasses and disallow them otherwise.

Ordering is another example of a typeclass where you may not want coherence.

I agree, but the issue with incoherence people keep mentioning involves ordering and dictionaries.

I 100% think that, in Scala like in ML, one appropriate solution should ensure the type of dictionaries depends on the ordering, so that dictionaries with different orderings have incompatible types. See https://github.com/chrisokasaki/scads/blob/master/design/heaps.md for a sketch, though that shows some issues. Support for ML applicative functors is another missing piece (see https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/24/slides/derek.pdf for why we care).

[neko-kai]

@Blaisorblade Are you sure Scala doesn't support applicative functors? You can share types trivially:

import scala.reflect.runtime.universe
import scala.reflect.api.Universe

trait Big { self =>

  val u: Universe
  val collab1: Collab1 { val u: self.u.type }
  val collab2: Collab2 { val u: self.u.type; val collab1: self.collab1.type }

  def tpe: u.Type = {
    val custom: collab1.MyCustomType = collab2.myCustomType
    val t: u.Type = custom.tpe
    t
  }
}

trait Collab2 { self =>
  val u: Universe
  val collab1: Collab1 { val u: self.u.type }

  def myCustomType: collab1.MyCustomType = collab1.MyCustomType(u.weakTypeOf[this.type])
}

trait Collab1 {
  val u: Universe

  case class MyCustomType(tpe: u.Type)
}

object Big {
  def apply
    (u0: Universe)
    (collab10: Collab1 { val u: u0.type })
    (collab20: Collab2 { val u: u0.type; val collab1: collab10.type }) =
    new Big { self =>
      final val u: u0.type = u0
      final val collab1: collab10.type = collab10
      final val collab2: collab20.type = collab20
    }
}

object Main extends App { self =>
  final val collab1 = new Collab1 { final val u: universe.type = universe }
  final val collab2 = new Collab2 { final val u: universe.type = universe; final val collab1 = self.collab1 }

  println(Big(universe)(collab1)(collab2).tpe)
}

What else is missing?

[Blaisorblade]

Your example doesn’t show an applicative functor, but since BIg.apply is fully transparent, the distinction between applicative and generative disappears. Applicative functors must work even when the functor’s return signature contains abstract interfaces. Here’s an example inspired from Derek Dreyer’s slides:

trait SetModule[Elem] {
  type Set
}
// we’d want this to be an applicative functor:
implicit def mkTreeSet[T: Ord]: SetModule[T] = new SetModule { /* ... */ }
//object TreeSet { def apply[T](x: T): SetModule[T] = mkTree
def singleton[T](x: T)(implicit sm: SetModule[T]): sm.Set
def merge[T](implicit sm: SetModule[T])(ts1: sm.Set, ts2: sm.Set): sm.Set
merge(singleton(1), singleton(2)) // won’t typecheck, but it could with applicative functors, because each implicit call to mkTreeSet[Int] will produce a distinct Set member, tho they will all be in fact the same

Most Scala programmers would also dispute “trivially”, but that’s a separate issue.

[odersky]

Here might be a possible scheme to support local coherence:

In a context bound like [F[_] : Monad : Traverse], the compiler should check that any type argument for F[_] provides the same implementation for any common superclass of Monad and Traverse. The common superclass of Monad and Traverse being Functor, this means we have to check for any type instance of F[_] that its Monad and Traverse implementations coincide for map. For ground types like List this can be checked by analyzing implicit definitions for the type. E.g.

class ListFunctor extends Functor[F[_]] { def map ... }
implicit object ListFunctor extends ListFunctor
implicit object ListMonad extends ListFunctor ...
implicit object ListTraverse extends ListFunctor ...

In a setup like this, the compiler can check that ListMonad and ListTraverse coincide for Functor, provided neither of them overrides map. For type parameters used as type arguments the property can be assumed transitively. E.g. if F above is passed to another parameter that has a : Monad : Traverse constraint, local coherence is already assumed.

It's an open question whether local coherence should be required for all context bounds [T : A : B], or whether we want an "opt-in" solution that requires special syntax such as [T : A & B] to indicate that T must be locally coherent for A and B and leave [T : A : B] as it is now without the requirement.

[neko-kai]

Another question would be – should a user be able to call a coherent-bound function with incoherent instances via .explicitly? If compiler has a green light on choosing arbitrary instance, behavior of such a call would be unpredictable – as such, IMO the programmer shouldn't be allowed that. In that case, I think, coherent-bounds shouldn't be the default – since it wouldn't be possible to override them if required.

NB: Odersky's proposal above was possibly derived by my recent comment in dotty / contributors (https://github.com/lampepfl/dotty-feature-requests/issues/4#issuecomment-419877645) (https://contributors.scala-lang.org/t/dotty-type-classes/2241/40)

[odersky]

@kaishh I agree, coherence needs to be enforced for explicit as well as implicit arguments.

But there is already a way to avoid coherence: use implicit parameters directly:

def f[X: A: B](...) // coherent
def f[X](...)(implicit ev1: A[X], implicit ev2: B[X]) // no coherence requirement

[buzden]

How then would you express the following bound: give me the context bound for X with A and B coherent and C possibly not coherent with others? Something like the following?

def f[X: A:B](...)(implicit evC: C[X])

Then what about two coherent pairs of A coherent with B and C coherent with D where two pairs are not obliged to be coherent with each other? Constraint like X: A&B : C&D in terms of &-for-context-bounds.

Or, maybe, such kind of bounds are never needed in practice?

[neko-kai]

@Blaisorblade Thanks, I got the distinction now! For your example to work though, the implicit def MUST be proven RT and the definition of a singleton type would have to change as well to become recomputable.

@odersky Yes, although, people would opt for shorter syntax without understanding the implications – I'm not sure it's SO harmful, as there shouldn't be a lot of incoherence between inheritors of the same base class in any reasonable class hierarchy, but still. Also, there must be a syntax for coherent summons that don't fit into context bounds:

def f[F[_]: Traverse](implicit ME: MonadError[F, Throwable])

e.g.:

def f[F[_]: Traverse](implicit ME: Coherent[MonadError[F, Throwable]])

@buzden In this proposal, instances may only be coherent in relation to their own base classes, not to each other. So all the coherent bounds that share base classes have to be coherent between each other, there's no way to summon several distinct sets for the same type.

[Jasper-M]

You can use context bounds for MonadError in dotty if you want.

def f[F[_] : [F[_]] => MonadError[F, Throwable]]

In Scala 2 too, strictly speaking...

def f[F[_] : ({type L[F[_]] = MonadError[F, Throwable]})#L]

[LukaJCB]

Hmm, I find it a bit counter intuitive that under this proposal def foo[A: Bar: Baz]: A no longer means the same thing as def foo[A](implicit ev1: Bar[A], ev2: Baz[A].

Not sure what to do in the case of explicitly, need to think about that a little bit more.

[odersky]

Hmm, I find it a bit counter intuitive that under this proposal def foo[A: Bar: Baz]: A no longer means the same thing as def foo[A](implicit ev1: Bar[A], ev2: Baz[A].

Yes, that's a downside. So maybe using a special syntax for coherent context bounds is preferable, after all.

[LukaJCB]

Yes, that's a downside. So maybe using a special syntax for coherent context bounds is preferable, after all.

What about using a marker trait like in your original proposal instead?

[odersky]

What about using a marker trait like in your original proposal instead?

I am not sure what that would look like?

[neko-kai]

After thinking some more, I'm now in favor of making local coherence default for both context bounds and parameter sections, and requiring user to request incoherence explicitly via some syntax, e.g.

def x[F[_]](implicit F: Monad[F] with Incoherent)

or

def x[F[_]](implicit F: Incoherent[Monad[F]])

Also, the list of base classes checked for coherence should obviously exclude AnyRef etc.

[LukaJCB]

I am not sure what that would look like?

What I mean by that is that if you use traits that extend the marker trait Typeclass then coherence is always assumed for both context bounds and parameter sections. @kaishh's suggestion also makes sense to me.

[odersky]

What I mean by that is that if you use traits that extend the marker trait Typeclass then coherence is always assumed for both context bounds and parameter sections. @kaishh's suggestion also makes sense to me.

I think we should never assume coherence without proof. If it's not checked, it's not there. If one absolutely needs an escape hatch, it could be via an @unchecked... annotation or similar, to make it clear that it's a potential soundness hole.

I am reluctant to introduce more marker traits to signify a property that is not strictly speaking a type. We did that with Singleton but if you think it through it has problems. E.g. what is the meaning of type-abstracting over a marker trait?

Finally, I am not convinced that the best way to model coherence is as a property between a class and its base class. That would flag any type class that overrides a method in its base class as incoherent. I think that would conflict with common idioms like Monad implementing map in terms of flatMap and pure. It seems more useful to me to restrict the problem to different type classes that share a common baseclass.

[buzden]

I think we should never assume coherence without proof.

As far as I understand, we should never talk about blind assuming when we are talking about local coherence, since it can be checked locally each time it is used, i.e. if a function with context-bounded parameters requires local coherence, we can check it at each use of this function. The need of this is clear and practical: it allows such a function to use different functions from required typeclass instances without worrying about incompatibility between their implementations. Solution seems to be existing: we need some syntax to distinguish whether function requires local coherence or not and we need to define clearly semantics and defaults. Maybe, other solutions exists too.

But if we talk about assuming, we are talking about global coherence. Are there any practical usages of it (except the fact that for some type there only one typeclass instance implementation exists that follows all the restrictions for the typeclass)? Sorry, if this question seems dumb.

[LukaJCB]

I think we should never assume coherence without proof. If it's not checked, it's not there. If one absolutely needs an escape hatch, it could be via an @unchecked... annotation or similar, to make it clear that it's a potential soundness hole.

I'm sorry, I worded that badly, what I meant was that coherence should always be checked in those cases.

I am reluctant to introduce more marker traits to signify a property that is not strictly speaking a type. We did that with Singleton but if you think it through it has problems. E.g. what is the meaning of type-abstracting over a marker trait?

Finally, I am not convinced that the best way to model coherence is as a property between a class and its base class. That would flag any type class that overrides a method in its base class as incoherent. I think that would conflict with common idioms like Monad implementing map in terms of flatMap and pure. It seems more useful to me to restrict the problem to different type classes that share a common baseclass.

That's fair. My preference would be to have that property be defined at the declaration-site instead of at the use-site. I think an explicit opt-out via @unchecked annotation or @kaishh's suggestion of Incoherent are a great idea :+1:

[odersky]

I'm sorry, I worded that badly, what I meant was that coherence should always be checked in those cases.

Ah, ok, I see what you mean now 😄

My preference would be to have that property be defined at the declaration-site instead of at the use-site.

I don't see how that could work. At the declaration site you'd be effectively checking global coherence, with all the problems that come with it. Local coherence is inherently a use site property. If I pass a type T and implicit instances A[T] and B[T] then A and B have to agree on how their common parts are implemented. That's tied to what I pass as arguments, so I would understand it as a use site property.

[LukaJCB]

I don't see how that could work. At the declaration site you'd be effectively checking global coherence, with all the problems that come with it. Local coherence is inherently a use site property. If I pass a type T and implicit instances A[T] and B[T] then A and B have to agree on how their common parts are implemented. That's tied to what I pass as arguments, so I would understand it as a use site property.

Right, sorry again, I was talking about the syntactical property not the semantical. The check should still be done at use-site.

I was just trying to voice, that in the event that we can't check local coherence by default, my preference would be something like this:

trait Functor[F[_]] { ... }

// Setting the "local coherence flag" at declaration-site
trait Applicative[F[_]] extends Functor[F] with CoherentInheritance { ... }
trait Traverse[F[_]] extends Functor[F] with CoherentInheritance { ... }

def Foo[F[_]: Traverse: Applicative] = ...

Over

trait Functor[F[_]] { ... }

trait Applicative[F[_]] extends Functor[F] { ... }
trait Traverse[F[_]] extends Functor[F] { ... }

// Setting the "local coherence flag" at the use-site
def Foo[F[_]: Traverse & Applicative] = ...

I hope that we don't have to do either and can do the checking by default and allow opting as had been mentioned earlier. :)

[rkrzewski]

IMHO an annotation on a type at use site seems to be the least intrusive way of activating the escape hatch.

def foo[F[_]](implicit F: Functor[F] @uncheckedCoherence)

[LukaJCB]

@rkrzewski Fully agreed :+1:

[LukaJCB]

@odersky Is there any update on this? :)