Think about type class/implicits encoding

[adelbertc]

Type classes are a widely used tool in Scala, both in the standard library (scala.math.Ordering) and in popular libraries like Cats, Scalaz, Spire, FS2, etc.

The obvious encoding of type classes via implicits has shortcomings, which I wrote about at length here. There are related issue tickets in Cats and Scalaz.

@djspiewak has written up a proposal for a type class encoding that requires language chances to the current Scala language.

I don't have any concrete ideas atm besides what Daniel has written about, nor am I necessarily advocating for global coherence like Haskell does, but I would like to see investigations into a better encoding of type classes in a future Scala that would accommodate the use cases above.

[odersky]

Thanks for putting this issue on the radar! One question: In your post, would it be acceptable to force the user to explicitly declare combinations of type classes that share an ancestor. E.g.

trait TraversableMonad[F[_]] extends Monad[F] with Traverse[F]

implicit def MonadAndTraverse[F[_]](
  implicit m: Monad[F],
  implicit t: Traverse[F]): TraversableMonad[F] = 
  new TraversableMonad[F] {
    def map[A, B](fa: F[A])(f: A => B): F[B] = m.map(fa)(f)
    def ap[A, B](f: F[A => B])(fa: F[A]): F[B] = m.map(f)(fa)
    def pure[A](x: A): F[A] = m.pure(x)
    def flatMap[A, B](fa: F[A])(f: A => F[B]): F[B] = m.flatMap(fa)(f)
    def traverse[G[_]: Applicative, A, B](fa: F[A])(f: A => G[B]): G[F[B]] = t.traverse(fa)(f)
  }

It is somewhat tedious to write all these forwarder methods, but it's a one off cost. Moreover there are some ideas for language features to make this less tedious. E.g., using a hypothetical export feature, we might be able to write something like this.

implicit def MonadAndTraverse[F[_]](
  implicit m: Monad[F],
  implicit t: Traverse[F]): TraversableMonad[F] = 
  new TraversableMonad[F] { export m._; export t._ }

The question is, whether in principle the discipline of closing all inheritance triangles that way is feasible. Given Cats, how many combiners would we need? What about foreseeable extensions to Cats?

[djspiewak]

@odersky In the Cats scenario, I don't think that many combiners are needed. Naively, Functor <: Applicative <: Monad <: Traverse, so that's something like 2n - 1 = 7 combiners. Of course, this is ignoring "side" typeclasses like FlatMap, so really there is more growth here. Also, as soon as you start having more and more specialized typeclasses built atop the generic hierarchy (e.g. fs2's Suspendable, Catchable, Async, and so on), the growth will probably quickly get out of hand. It's not the boilerplate per se that I'm specifically objecting to, though requiring it would certainly be annoying, but the fact that the implicit resolution is (in principle) exponential in the number of candidate instantiations.

But more significantly, I'm not certain that your proposal entirely resolves the problem. Consider the classic issue with MTL-style monad transformer typeclasses (which are, as I mentioned at Scala Days, basically the current state of the art in pleasant stackable effects):

def foo[F[_]](implicit MS: MonadState[F, String], MO: MonadOption[F]): F[Int] =
  Monad[F].pure(42)

(for context, object Monad { def apply[F[_]](implicit F: Monad[F]) = F } is a common idiom here)

So the problem here is figuring out where we get the Monad instance from: derived from MonadState or MonadOption? And this is where the forwarder idea becomes completely intractable, because if I understand your idea correctly, we would need forwarders for every possible combination of effects, which is clearly intractable.

My proposal (which @adelbertc linked) proposes we resolve this by tagging instances with "compatible indirect derivations" into "coherence domains". Its primary downside is it doesn't provide any actual checking for this behavior, so it's possible to generate scenarios where the runtime behavior may actually be undefined, simply by falsely declaring two incompatible instances are in fact compatible. I'm curious as to your thoughts on this proposal.

To be clear on my opinion here…  I don't much care what approach we take, so long as it is scalable and addresses the issue in some way. My primary concern is that we don't go the "full Haskell" route and simply forbid local instances, since I'm really not a fan of the consequences of that design decision. But given the rest of Scala's design space, that doesn't seem to be particularly plausible design route anyway. :-)

[odersky]

Naively, Functor <: Applicative <: Monad <: Traverse, so that's something like 2n - 1 = 7 combiners

According to my count, it's just Applicative/Traverse and Monad/Traverse, so that makes 2. The others don't form triangles (?)

I am skeptical about the monad transformer typeclass approach for stackable effects, at least as far as dotty is concerned. I believe we will have much better ways to model most effects as implicit capabilities. There are a few effects that influence control flow which cannot be modelled as capabilities. But these should be few, and therefore manual combiners may again be a feasible option.

[djspiewak]

In @adelbertc's example article, you're correct that only Monad and Traverse form a triangle. The real hierarchy is somewhat more complex. Assuming typeclasses are implemented via unique instances and inheritance (the current Cats and Scalaz encoding), only triangles (literally the diamond problem in a different guise) exhibit this issue. Other encodings (such as the old Scalaz 6 encoding) can exhibit issues with other structures.

I am skeptical about the monad transformer typeclass approach for stackable effects, at least as far as dotty is concerned. I believe we will have much better ways to model most effects as implicit capabilities. There are a few effects that influence control flow which cannot be modelled as capabilities. But these should be few, and therefore manual combiners may again be a feasible option.

I'm skeptical about monad transformers as well, and really so is the entire Haskell community. This is why MTL exists in the first place. As I mentioned at Scala Days, your description of capability-based effects in Dotty sounds almost exactly like what exists in MTL today. The type signature I gave is an example of this. Rather than reading that type signature in terms of a stack of effects, just look at MonadState and MonadOption as being capabilities: the former is the capability of purely threading state through sequential computation, and the latter is the capability of nullability in sequential computation.

Regardless of what approach Dotty uses, I think we're going to have to solve this problem. Think about my example again in highly abstract terms. Given two capabilities A and B, where A = A' ∪ C and B = B' ∪ C, and some expression which requires capability C, how do you get C unambiguously? MTL provides a great example of this, both because it's a practical implementation of a capability-based stackable effect system via typeclasses, and because it demonstrates that the control-flow affecting effects (yay, english…) are actually quite numerous.

[adelbertc]

Some scattered thoughts I have:

@djspiewak : My proposal (which @adelbertc linked) proposes we resolve this by tagging instances with "compatible indirect derivations" into "coherence domains".

I wonder if we can have a subset(type) relationship across these domains, if that makes sense or is even a thing.

@odersky : According to my count, it's just Applicative/Traverse and Monad/Traverse, so that makes 2. The others don't form triangles (?)

While those are probably the most common ones, my concern is the general principle that the naive encoding of type classes via implicits/traits + subtyping does not work for type classes as we know it. Given that encoding, any given type class hierarchy must be linear/cannot branch/cannot share a common superclass.

@djspiewak : Rather than reading that type signature in terms of a stack of effects, just look at MonadState and MonadOption as being capabilities

Yep, Monad{Reader, Writer, State, Error} tend to be the "classic" type classes in MTL. In general though the approach can be seen as a way of encoding DSLs or effects in general, a couple folks have written about this:

• https://failex.blogspot.com/2016/12/tagless-final-effects-la-ermine-writers.html
• https://pchiusano.github.io/2014-05-20/scala-gadts.html
• http://typelevel.org/blog/2016/10/26/edsls-part-2.html

[odersky]

These are good points.

Given two capabilities A and B, where A = A' ∪ C and B = B' ∪ C, and some expression which requires capability C, how do you get C unambiguously?

We agree it should not matter how you get C. So, yes, it seems promising to convey that fact somehow to the type checker. If I take your example literally it would seem more natural to annotate the type or type constructor (C in this case), which should express something like:

"for each type instance of C the behavior of all implicit values of that type instance is the same".

We could get individual coherence domains by functorizing, i.e. make C into an inner class so that type instances are path dependent types that each can be implemented individually.

By contrast, the coherence domains you propose seem to attach uniqueness to the implicit instances instead of to the type they implement. That could also work, although I am not keen on some of the syntactic details. Also I am dubious about using types as tags like that. But that's just a gut reaction, which might change with exposure.

[djspiewak]

We could get individual coherence domains by functorizing, i.e. make C into an inner class so that type instances are path dependent types that each can be implemented individually.

At first glance, this sounds very similar to an idea that @milessabin has been exploring to constructively encode coherence via type intersection on inner types.

By contrast, the coherence domains you propose seem to attach uniqueness to the implicit instances not to the type the implement. That could also work, although I am not keen on some of the syntactic details. Also I am dubious about using types as tags like that. But that's just a gut reaction, which might change with exposure.

Phantom type tags are used a lot in type-level programming in Scala (and in Haskell), simply because Scala's type system is ultimately nominal rather than structural. Polymorphism makes this complicated obviously, but it's a pretty well-used idiom, which is why I reached for it. I didn't want to introduce a secondary but non-orthogonal mechanism for uniqueness tagging when named types already have that mechanism defined in a relatively robust fashion.

The other advantage with unifying coherence tags with types is that it allows the computation of tags as a consequence of type resolution. The big problem here is this obviously opens up a very interesting can of worms and a secondary cycle in the type resolution (where type computation influences coherence domains which in turn influences implicit resolution which in turn influences type computation). It wouldn't be the first such cycle, but adding another is still enough to personally give me pause.

I would vastly prefer a mechanism for constructing coherent definitions rather than declaring coherent instances. It would be less flexible, but more checkable and likely introduce less baggage. The conceptual problem I see with working at this from the definition site is it feels fundamentally incompatible with local instances, unless we can encode it in the dependent type.

Also, in case we go with annotating type definitions, what would be a good way to do it? The most direct one would be a modifier or annotation, but what should its name be?

[odersky]

simply because Scala's type system is ultimately nominal rather than structural.

Just to argue the point :-), in fact DOT has shown that Scala's type system is ultimately structural, where nominal types can be modelled as abstract types.

would vastly prefer a mechanism for constructing coherent definitions rather than declaring coherent instances. It would be less flexible, but more checkable and likely introduce less baggage. The conceptual problem I see with working at this from the definition site is it feels fundamentally incompatible with local instances, unless we can encode it in the dependent type.

Can you give an example?

[djspiewak]

Just to argue the point :-), in fact DOT has shown that Scala's type system is ultimately structural, where nominal types can be modelled as abstract types.

Well at that point the tag in the nominal type comes out of the uniqueness of the path-dependent instantiation, if I understand correctly. Either way, "nominative with heavy structural features" or "structural with nominal encoding", you still end up with tags somewhere. :-)

would vastly prefer a mechanism for constructing coherent definitions rather than declaring coherent instances. It would be less flexible, but more checkable and likely introduce less baggage. The conceptual problem I see with working at this from the definition site is it feels fundamentally incompatible with local instances, unless we can encode it in the dependent type.

Can you give an example?

If you're bringing in a generic MonadState and a generic MonadOption, as in my example above, and you don't declare anything else about those instances, how do you know that the specific instantiations given were declared with a coherent Monad? The point that I'm vaguely conceptually grasping at is that the type signature I gave doesn't have enough information to resolve this problem unless you chuck out local instances entirely, which is obviously not an answer. So, any solution to this would require a slightly richer type signature at the "usage" site (by which I mean, the implicit parameter block).

[odersky]

you're bringing in a generic MonadState and a generic MonadOption, as in my example above, and you don't declare anything else about those instances, how do you know that the specific instantiations given were declared with a coherent Monad?

It would have to be that Monad itself is declared to be coherent:

coherent trait Monad[F[_]] { ... }

(Not sure about the term coherent yet, just to pick a concrete name for this). If Monad was declared like this, we'd assume that two implicit values of the same Monad type would be behaviorally equivalent. Whether and how to check that is another question.

[djspiewak]

Oh I see what you mean. Still an assertion rather than a construction. Doesn't this effectively selectively disable local instances though? Because what you're saying is that in any case where there are multiple Monad[F] (for a given F), they must all be the same. Which is to say, indistinguishable from the notion of a globally unique Monad[F].

[djspiewak]

Also, just to play devil's advocate, there are numerous instances where this wouldn't be as nice as it could be. Consider the classic example of Monoid[Boolean]. You wouldn't want to declare Monoid as coherent – because it might not be! – but there's nothing to stop it from being involved in diamonds like the ones we've been talking about.

[odersky]

Consider the classic example of Moniod[Boolean]. You wouldn't want to declare Monoid as coherent – because it might not be! – but there's nothing to stop it from being involved in diamonds like the ones we've been talking about.

Can you flesh that out a bit for me? I don't see yet what you are getting at.

[djspiewak]

Monoid[Boolean] has two equally valid implementations: one defined by (true, &&) and the other by (false, ||). This makes it a decent example of the usefulness of local instances. We wouldn't want to declare Monoid as coherent, because it isn't coherent.

But it isn't difficult to imagine Monoid being involved in a diamond similar to what we constructed with MonadState and MonadOption. I mean, if nothing else, Monad is simply a higher-order Monoid. So the diamond problem remains even for typeclasses which have clear and useful incoherence.

[odersky]

Thanks for explaining. How would you handle the Monoid case using coherence domains?

[djspiewak]

Under normal circumstances, you would just allow the incoherence. If you define two instances for Monoid[Boolean], and you ask for a Monoid[Boolean], well that's ambiguous and you would get the same error you do today. Where coherence domains differ is they would make something like this possible:

// presumably MonoidFoo[a] <: Monoid[a] and MonoidBar[a] <: Monoid[a]
def example[A](implicit[_] AF: MonoidFoo[A], AB: MonoidBar[A]) = Monoid[A].zero

(facetious examples here with Foo and Bar, but generalize from the Monad example earlier)

Since we've declared (via the implicit[_] syntax) that the MonoidFoo instances and MonoidBar instances are coherent, we can discard the ambiguity on Monoid[A] and just "pick" one of the instances. At the declaration site, it would look something like this:

// just some arbitrary type tag
class U

implicit[U] val mfb: MonoidFoo[Boolean] = ...
implicit[U] val mbb: MonoidBar[Boolean] = ...

example[Boolean]   // compiles and runs

This is similar to your idea of declaring coherent, the difference is that we can declare coherence at the alias site (rather than where the type is declared), and we get the ability to define different domains of coherence, rather than being stuck with a single implicitly-global one.

To be clear in the above example, since I elided the implementations, mfb and mbb would need to be using a specific implementation of Monoid[Boolean]. They're asserting by saying they're both in coherence domain U that the implementation they have chosen is the same (e.g. maybe the (true, &&) one), but we can't check that assertion. The way they choose their implementation is going to come down to simply which one they extend in their implementation.

[odersky]

Since we've declared (via the implicit[_] syntax) that the MonoidFoo instances and MonoidBar instances are coherent, we can discard the ambiguity on Monoid[A] and just "pick" one of the instances. At the declaration site, it would look something like this:

implicit[_] seems to be too sweeping in that it forces all following implicits to be coherent, right? What if we only want a subset? Also it would be yet another use of the _ :weary:

[odersky]

Here's a more worked out example how one could express Monoids with coherency attached to the type. Since coherency is inherited, i.e. it's a condition that has to be maintained for all subtypes, it seems more logical to pick a marker trait than an annotation for it. So,

trait Cap[T] extends Coherent

would force all instances of Cap or its subtypes to be coherent. Now, to monoids. The Monoid trait itself would not be declared coherent:

package kernel
trait Monoid[T] ...

But I can declare a coherent subtrait:

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

Here are some instances:

implicit val mfb: Canonical.MonoidFoo[Boolean] = ...
implicit val mbb: Canonical.MonoidBar[Boolean] = ...

And here's the use site:

def example[A](implicit AF: MonoidFoo[A], AB: MonoidBar[A]) = Canonical.Monoid[A].zero

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

One nice aspect about attaching coherence to types is that it works well with the phantom types proposal. (see https://github.com/lampepfl/dotty/pull/1408). We plan to model effect capabilities as phantom types, and there will be several other usages as well (e.g. the =:=, <:< types). Phantom types have the property that they are compile-time only: all their values are erased. So if you had an implicit parameter of type =:=, say, the runtime argument would be erased. This makes all phantom types coherent by design, which is exactly what we need for capabilities.

[odersky]

I have added #2040, which reflects the current state of discussion of phantom types.

[mandubian]

Just my 2cts contrib to this topic... As a side-reflection of my Kind-Polymorphism scalac study/PR, I had used a KindPolymorphic List to reify behaviors/typeclasses/laws of a structure in a single implicit structure.

https://github.com/mandubian/scala/blob/topic/kind-poly-v1/test/files/run/kind-poly9.scala#L153-L203

Then, I could use that to find a behavior/typeclasse/law associated to a structure but also scope it (to choose Monoid of Numeric for example) and imagine funnier things like documentation generation, structure laws/typeclasses comparisons and anything you can imagine...

This was really interesting, hadn't the classic limitations of Typeclass hierarchy by inheritance... Except its runtime cost of manipulating those "List of Laws"...

[djspiewak]

implicit[_] seems to be too sweeping in that it forces all following implicits to be coherent, right? What if we only want a subset? Also it would be yet another use of the _ 😩

Well, it's not another use of _ really. It's the same use as in the type Foo[_], and would have the same desugaring. But I guess that is a slippery slope from the perspective of the "surface" language.

Here's a more worked out example how one could express Monoids with coherency attached to the type. snip

That looks pretty interesting, actually. What you're doing there is conceptually newtyping the more general, potentially-incoherent Monoid into a coherent variant of the same. I generally hate "magical" marker traits, but this works out fairly well since the inheritance matches well with the standard encodings.

Encoding variable coherence domains by using a class rather than an object and relying on the path-dependence to disambiguate is pretty cool, and subjectively feels like it fits well with Scala's core calculus. This really is effectively the same thing as my implicit[U] coherence domain idea, but at the declaration site rather than the aliasing site (call site?).

One concern that I have is if we push coherence to the declaration site in the form of an assertion rather than a construction, library authors like Cats and Scalaz are just going to mark everything as Coherent. That's not necessarily wrong, but it does mean that none of their types will ever be useful in a local-instance context (though obviously they will still obey scoping rules). So despite Monoid being our example of useful incoherence, I have absolutely no doubt that both scalaz.Monoid and cats.Monoid would extend Coherent the moment this feature is introduced. Perhaps that's an indication that incoherence is less useful than I contend, I'm not sure.

[OlivierBlanvillain]

I think the language could also benefit from a mechanism to (selectively) disable any form of implicit ambiguity in user code.

Non-coherent implicits are rather fragile in their current state because of the many ways of silently breaking things. By adding/deleting implicit arguments, adding/deleting imports, or simply moving things around, one can change implicit resolution in a way that affects run-time semantics.

The solution I have in mind is a NonCoherent annotation/trait that would tell the compiler to emit an error if any of the implicit precedence rules affects the resolution of instances for annotated types.

[odersky]

One concern that I have is if we push coherence to the declaration site in the form of an assertion rather than a construction, library authors like Cats and Scalaz are just going to mark everything as Coherent. That's not necessarily wrong, but it does mean that none of their types will ever be useful in a local-instance context (though obviously they will still obey scoping rules). So despite Monoid being our example of useful incoherence, I have absolutely no doubt that both scalaz.Monoid and cats.Monoid would extend Coherent the moment this feature is introduced. Perhaps that's an indication that incoherence is less useful than I contend, I'm not sure.

Maybe one way to improve the situation is if we put certain fundamental type classes which naturally admit several different implementations in the standard library. Monoid is probably a good example. So there would be a non-coherent Monoid somewhere in Scala and it would then be natural for cats or scalaz's Monoid to extend it with a coherent Monoid.

[djspiewak]

Maybe one way to improve the situation is if we put certain fundamental type classes which naturally admit several different implementations in the standard library. Monoid is probably a good example. So there would be a non-coherent Monoid somewhere in Scala and it would then be natural for cats or scalaz's Monoid to extend it with a coherent Monoid.

I think that would be a natural solution, as well as have other benefits. It would certainly be nice to have a single type which represents Monad, as opposed to the current situation where there are no fewer than five identical ones in common use.

[lambdista]

In my humble opinion it would be so nice having all fundamental type classes in the standard library, not only those which admit several different implementations.

Another "dream" I have is having a collection library in terms of instances of those type classes in place of being expressed as an OO hierarchy, as they are now. However, I would still be fine with using an external lib for it.

[alexandru]

@lambdista cats-core is about 3.4 MB and cats-kernel is about 4.6 MB and this is a library in active development that can't yet guarantee source backwards compatibility. One can argue that not all of those type-classes are needed, but many people disagree, as most of those are fundamental. And that's a lot to add to the standard library, which is then set in stone, unless another round of deprecations happen in a couple of years after 2 or 3 major Scala versions. And no standard library that I know of has aged well, unless it broke people's code and expectations.

[aisven]

Naively asked, after a long evening of reading, to me it is striking that Monoid[Boolean] simply seems not explicit enough. It feels as if it is simply not enough to declare a Monoid. It also needs:

• single most natural operation for combining values
• identity element

Could the whole scoped coherence approach not be spared if simply a Monoid would have to be defined more explicitely including the combine operation and the identity element?