Add EqK, SemigroupK, and MonoidK?

[ceedubs]

Currently the "kinded" versions of Eq, Semigroup, and Monoid (that is, EqK, SemigroupK, and MonoidK) live in Cats. Should they live in Algebra to be with their non-universal counterparts?

One benefit of having the K versions in Algebra is that we could add a conversion like implicit def fromEqK[F[_]:EqK, A:Eq]: Eq[F[A]] in the Eq companion object (and similarly for Semigroup and Monoid). Right now we can define these in Cats, but we don't have a companion object we could add them to where implicit search would find them.

[ceedubs]

As @mpilquist points out, the conversion I mentioned might not actually be a good idea. https://gitter.im/non/cats?at=5612d2a9ce6e633c45187c11

[johnynek]

It actually seems to me that EqK vs SemigroupK and MonoidK are a bit different. EqK is like an Eq factory, if you will, while SemigroupK and MonoidK are semigroups and monoids that are independent of the type, such as List[T] (but I don't know other examples than the free-semigroup off hand). As a note, what are examples of instances of these kinds of semigroups?

Anyway, these seem like they could be here to me, but I don't recall ever really reaching for these (i.e. wanting to write code that is generic over SemigroupK/MonoidK).

[ceedubs]

@johnynek you are definitely right about EqK being a different breed than SemigroupK and MonoidK. There has been discussion about changing them to not use the same K convention.

Another example of a free semigroup is Option with orElse as the combine function. Note that this is a different Option semigroup than the default one provided by Cats (and changing this has been discussed a couple times too).

As far as when we would reach for SemigroupK instead of Semigroup: this is a good question. The only thing that comes to mind right now, is you could follow a convention that whenever a SemigroupK[F] exists, Semigroup[F[A]] (for all A) should be consistent with it. As I mentioned, Cats currently doesn't follow this convention.

Currently the only place I really reach for EqK is in Cats tests. However, I've raised a concern about EqK being overly constraining for these tests.

I think I'm now questioning whether these K type class instances really bring much value. I think @non and @mpilquist have been involved in creating them. Do you two have some examples of how they can be more helpful than their non-K counterparts?

[mpilquist]

@ceedubs MonoidK/SemigroupK correspond to Haskell's PlusEmpty/Plus. The former, when joined with Applicative yields the Alternative type class, and when joined with Monad yields MonadPlus.

[non]

So I think the correct term for things like SemigroupK and MonoidK is universal algebra. I don't think there is necessarily a good name for EqK although I've called it a contingent algebra.

I'm not sure how necessary EqK is (and it may be overly constraining sometimes) but it seems to fit a broad category of usages I've seen. I agree with @mpilquist that SemigroupK and MonoidK are mostly useful when you are abstracting over types with a F[_] shape (such as Option, List, etc.).

[adelbertc]

In response to the discrepancy between the "derived" non-kinded versions of the kinded type classes and the non-derived one, it seems this falls into the case where a given type may have several valid instances of a particular type class.

For that reason I think we either need to somehow universally agree that for 99% of use cases this is the specific instance we want, or not provide a default at all and have people explicitly define it (perhaps via https://github.com/mpilquist/local-implicits )

[johnynek]

I wonder if:

trait UniversalSemigroup[F[_]] {
  def combine[A](a: F[A], b: F[A]): F[A]
}

trait UniversalMonoid[F[_]] extends UniversalSemigroup[F] {
  def empty[A]: F[A]
}

trait Contingent[TC[_], F[_]] {
  def for[A](implicit tc: TC[A]): TC[F[A]] 
}
// EqK[List] == Contingent[Eq, List] 

would be a decent way to go.

[johnynek]

Also, not sure these need to be here at all. Seems like Cats is where these belong to me.

[tixxit]

Agree that these belong in cats (and are, in fact, there). Can we close this? @non ?

[ceedubs]

This was opened before cats-kernel existed. I don't think it would make much sense for this to be in algebra now. Closing out.