SplitLaw doesn't hold in general

[peterneyens]

When you run our current SplitLaw for Kleisli[Either[String, ?], ?, ?] it fails the splitInterchange law.
@fthomas already mentioned in #232 that he wasn't sure that it was sound.

If you add the following to KleisliTests you can see it fail.

{
  type StringOr[A] = Either[String, A]
  
  // SI 2712 workarounds
  implicit val EqFAA     = implicitly[Eq[Kleisli[StringOr,Int,Int]]]
  implicit val EqFACB    = implicitly[Eq[Kleisli[StringOr,(Int, Int),Int]]]
  implicit val EqFACBC   = implicitly[Eq[Kleisli[StringOr,(Int, Int),(Int, Int)]]]
  implicit val EqFACDBCD = implicitly[Eq[Kleisli[StringOr,((Int, Int), Int),(Int, (Int, Int))]]]
  
  implicit val invariant = Kleisli.catsDataFunctorForKleisli[StringOr, Int]
  implicit val iso = CartesianTests.Isomorphisms.invariant[Kleisli[StringOr, Int, ?]]
  
  implicit val ArbFAB = implicitly[org.scalacheck.Arbitrary[Kleisli[StringOr,Int,Int]]]
  
  implicit val catsDataArrowForKleisli = Kleisli.catsDataSplitForKleisli[StringOr]
  checkAll("Kleisli[Either[String, ?], Int, Int]", SplitTests[Kleisli[StringOr, ?, ?]].split[Int, Int, Int, Int, Int, Int])
}

I looked at it with @diesalbla and the law only seems to hold for commutative arrows.

[diesalbla]

The law for the split operation from the Split[F[_,_] type-class, together with the laws for the Arrow[_,_] type class, has an structure which is not that of the conventional Arrows, as explained here. Instead, it has the structure of a Commutative Arrow, which is described in the referred article. That these laws are more restrictive means that some instances of the trait Arrow[F[_,_]] for some types F will hold only the normal Arrow laws, but not the Commutative Arrow ones. In particular, the instance constructor implicit def catsDataArrowForKleisli[F[_]](implicit ev: Monad[F]): Arrow[Kleisli[F, ?, ?]] would not be a commutative arrow for Kleisli.

Equivalence between Commutativity and splitInterchange.

Using Haskell-like notation, we write *** for split and >>> for andThen, so we can express:

• The commutativity law as first f >>> second g == second g >>> first f for any f,g.
• The splitInterchange law is that (f *** g) >>> (h *** k) == (f >>> h) *** (g >>> k) for any f,g,h,k.

We can expand the splitChange law, first by unfolding the definition of ***, and then by using the functor law of first and second, as follows:

(f *** g) >>> (h >>> k)  == (f >>> h) *** (g >>> k)  
first f >>> second g >>> first h >>> second k == first (f >>> h) >>> second (g >>> k)
first f >>> second g >>> first h >>> second k == first f >>> first h >>> second g >>> second k

We omit parenthesis because >>> is associative. From there, we see that commutativity implies splitInterchange, because it allows to swap the middle terms second g and first h. Also, splitInterchange implies commutativity, because if we apply it to the particular case f=id, k=id, we can remove the terms first f and second k to leave just the commutativity law.

[diesalbla]

Looking at the history, it seems that @non wrote the original definitions of the type-classes, but the splitInterchange law was later added by @fthomas in PR #232, but he comments there that he was not sure about its correctness. Moving forward, I can see two redesign options.

The first option is to modify the inheritance hierarchy in the cats.arrow package: the trait Arrow should not inherit from Split, and add a class CommutativeArrow[F[_,_]] extending both Split and Arrow. The second option would be to simply remove the splitInterchange law. IMHO, the latter would just leave a hollow type class, so the former would be better.

Edited: In the first case, we can also remove the Split type-class altogether.

[ceedubs]

@kailuowang should this be assigned to 1.0? It seems like we might be down a problematic trajectory on this one.

[kailuowang]

@ceedubs I agree. assigned.

[kailuowang]

I vote for option 1 proposed by @diesalbla in #1567 (comment), whose analysis in this issue is, IMO, great work.

[edmundnoble]

I'm good with option 1 as well.

[peterneyens]

ArrowLaws already has a law covering the split method and overrides split.

We can make split a normal method of Arrow, drop the Split type class and add CommutativeArrow with the current splitInterchange law?

[diesalbla]

Since there is some agreement, i shall carry out through with option 1. This will include modifying the inheritance relations as described, as well with the laws, and updating the existing instances of Arror[M] to CommutativeArrow[X], where applicable.

[fthomas]

Sorry for chiming in so late in the conversation. I think @diesalbla's and @peterneyens' analysis is spot-on. My justification for adding splitInterchange in #232 was based on this proof where I mistakenly assumed second g >>> first f = first f >>> second g for the arrow exchange law (which holds for conventional arrows). But as @diesalbla already noted, this is the commutativity law of commutative arrows.

[peterneyens]

Fixed in #1766.