Strong profunctor laws based on category theory

laws/src/main/scala/cats/laws/StrongLaws.scala

@@ -4,23 +4,61 @@ package laws
 import cats.arrow.Strong
 import cats.syntax.profunctor._
 import cats.syntax.strong._
-import cats.instances.function._
 
 /**
  * Laws that must be obeyed by any `cats.functor.Strong`.
+ *
+ * See: [[https://arxiv.org/abs/1406.4823 E. Rivas, M. Jaskelioff Notions of Computation as Monoids, Chapter 7]]
+ * See: [[http://hackage.haskell.org/package/profunctors/docs/Data-Profunctor-Strong.html Haskell Data.Profunctor.Strong]]
  */
 trait StrongLaws[F[_, _]] extends ProfunctorLaws[F] {
   implicit override def F: Strong[F]
 
-  def strongFirstDistributivity[A0, A1, B1, B2, C](fab: F[A1, B1],
-                                                   f: A0 => A1,
-                                                   g: B1 => B2): IsEq[F[(A0, C), (B2, C)]] =
-    fab.dimap(f)(g).first[C] <-> fab.first[C].dimap(f.first[C])(g.first[C])
+  private def swapTuple[X, Y]: Tuple2[X, Y] => Tuple2[Y, X] = _.swap
 
-  def strongSecondDistributivity[A0, A1, B1, B2, C](fab: F[A1, B1],
-                                                    f: A0 => A1,
-                                                    g: B1 => B2): IsEq[F[(C, A0), (C, B2)]] =
-    fab.dimap(f)(g).second[C] <-> fab.second[C].dimap(f.second[C])(g.second[C])
+  /** first' == dimap swap swap . second' */
+  def firstIsSwappedSecond[A, B, C](fab: F[A, B]): IsEq[F[(A, C), (B, C)]] =
+    fab.first[C] <-> fab.second[C].dimap(swapTuple[A, C])(swapTuple[C, B])
+
+  /** second' == dimap swap swap . first' */
+  def secondIsSwappedFirst[A, B, C](fab: F[A, B]): IsEq[F[(C, A), (C, B)]] =
+    fab.second[C] <-> fab.first[C].dimap(swapTuple[C, A])(swapTuple[B, C])
+
+  /** lmap fst == rmap fst . first' */
+  def lmapEqualsFirstAndThenRmap[A, B, C](fab: F[A, B]): IsEq[F[(A, C), B]] =
+    fab.lmap[(A, C)]({ case (a, _) => a }) <-> fab.first[C].rmap[B](_._1)
+
+  /** lmap snd == rmap snd . second' */
+  def lmapEqualsSecondAndThenRmap[A, B, C](fab: F[A, B]): IsEq[F[(C, A), B]] =
+    fab.lmap[(C, A)]({ case (_, b) => b }) <-> fab.second[C].rmap[B](_._2)
+
+  private def mapFirst[X, Y, Z](f: X => Z)(cb: (X, Y)): (Z, Y) = (f(cb._1), cb._2)
+  private def mapSecond[X, Y, Z](f: Y => Z)(cb: (X, Y)): (X, Z) = (cb._1, f(cb._2))
+
+  /** lmap (second f) . first == rmap (second f) . first */
+  def dinaturalityFirst[A, B, C, D](fab: F[A, B], f: C => D): IsEq[F[(A, C), (B, D)]] =
+    fab.first[C].rmap(mapSecond(f)) <-> fab.first[D].lmap(mapSecond(f))
+
+  /** lmap (first f) . second == rmap (first f) . second */
+  def dinaturalitySecond[A, B, C, D](fab: F[A, B], f: C => D): IsEq[F[(C, A), (D, B)]] =
+    fab.second[C].rmap(mapFirst(f)) <-> fab.second[D].lmap(mapFirst(f))
+
+  private def assoc[A, B, C]: (((A, B), C)) => (A, (B, C)) = { case ((a, c), d)   => (a, (c, d)) }
+  private def unassoc[A, B, C]: ((A, (B, C))) => ((A, B), C) = { case (a, (c, d)) => ((a, c), d) }
+
+  /** first' . first' == dimap assoc unassoc . first' where
+   *   assoc ((a,b),c) = (a,(b,c))
+   *   unassoc (a,(b,c)) = ((a,b),c)
+   */
+  def firstFirstIsDimap[A, B, C, D](fab: F[A, B]): IsEq[F[((A, C), D), ((B, C), D)]] =
+    fab.first[C].first[D] <-> fab.first[(C, D)].dimap[((A, C), D), ((B, C), D)](assoc)(unassoc)
+
+  /** second' . second' == dimap unassoc assoc . second' where
+   *   assoc ((a,b),c) = (a,(b,c))
+   *   unassoc (a,(b,c)) = ((a,b),c)
+   */
+  def secondSecondIsDimap[A, B, C, D](fab: F[A, B]): IsEq[F[(D, (C, A)), (D, (C, B))]] =
+    fab.second[C].second[D] <-> fab.second[(D, C)].dimap[(D, (C, A)), (D, (C, B))](unassoc)(assoc)
 }
 
 object StrongLaws {

laws/src/main/scala/cats/laws/discipline/ArrowChoiceTests.scala

@@ -34,10 +34,13 @@ trait ArrowChoiceTests[F[_, _]] extends ArrowTests[F] with ChoiceTests[F] {
     EqFACBD: Eq[F[(A, C), (B, D)]],
     EqFADCD: Eq[F[(A, D), (C, D)]],
     EqFADCG: Eq[F[(A, D), (C, G)]],
-    EqFAEDE: Eq[F[(A, E), (D, E)]],
+    EqFDADB: Eq[F[(D, A), (D, B)]],
+    EqFCADB: Eq[F[(C, A), (D, B)]],
     EqFABC: Eq[F[A, (B, C)]],
-    EqFEAED: Eq[F[(E, A), (E, D)]],
     EqFACDBCD: Eq[F[((A, C), D), (B, (C, D))]],
+    EqFACDBCD2: Eq[F[((A, C), D), ((B, C), D)]],
+    EqFDCADCB: Eq[F[(D, (C, A)), (D, (C, B))]],
+    EqFCAB: Eq[F[(C, A), B]],
     EqFEitherABD: Eq[F[Either[A, B], D]],
     EqFEitherCoABC: Eq[F[A, Either[B, C]]],
     REqFEitherACD: Eq[F[Either[A, D], Either[C, D]]],

laws/src/main/scala/cats/laws/discipline/ArrowTests.scala

@@ -32,10 +32,13 @@ trait ArrowTests[F[_, _]] extends CategoryTests[F] with StrongTests[F] {
     EqFACBD: Eq[F[(A, C), (B, D)]],
     EqFADCD: Eq[F[(A, D), (C, D)]],
     EqFADCG: Eq[F[(A, D), (C, G)]],
-    EqFAEDE: Eq[F[(A, E), (D, E)]],
+    EqFDADB: Eq[F[(D, A), (D, B)]],
+    EqFCADB: Eq[F[(C, A), (D, B)]],
     EqFABC: Eq[F[A, (B, C)]],
-    EqFEAED: Eq[F[(E, A), (E, D)]],
-    EqFACDBCD: Eq[F[((A, C), D), (B, (C, D))]]
+    EqFCAB: Eq[F[(C, A), B]],
+    EqFACDBCD: Eq[F[((A, C), D), (B, (C, D))]],
+    EqFACDBCD2: Eq[F[((A, C), D), ((B, C), D)]],
+    EqFDCADCB: Eq[F[(D, (C, A)), (D, (C, B))]]
   ): RuleSet =
     new RuleSet {
       def name: String = "arrow"

laws/src/main/scala/cats/laws/discipline/CommutativeArrowTests.scala

@@ -33,9 +33,12 @@ trait CommutativeArrowTests[F[_, _]] extends ArrowTests[F] {
     EqFACBD: Eq[F[(A, C), (B, D)]],
     EqFADCD: Eq[F[(A, D), (C, D)]],
     EqFADCG: Eq[F[(A, D), (C, G)]],
-    EqFAEDE: Eq[F[(A, E), (D, E)]],
-    EqFEAED: Eq[F[(E, A), (E, D)]],
-    EqFACDBCD: Eq[F[((A, C), D), (B, (C, D))]]
+    EqFDADB: Eq[F[(D, A), (D, B)]],
+    EqFCADB: Eq[F[(C, A), (D, B)]],
+    EqFACDBCD: Eq[F[((A, C), D), (B, (C, D))]],
+    EqFACDBCD2: Eq[F[((A, C), D), ((B, C), D)]],
+    EqFDCADCB: Eq[F[(D, (C, A)), (D, (C, B))]],
+    EqFCAB: Eq[F[(C, A), B]]
   ): RuleSet =
     new DefaultRuleSet(name = "commutative arrow",
                        parent = Some(arrow[A, B, C, D, E, G]),

laws/src/main/scala/cats/laws/discipline/StrongTests.scala

@@ -12,7 +12,6 @@ trait StrongTests[F[_, _]] extends ProfunctorTests[F] {
   def strong[A: Arbitrary, B: Arbitrary, C: Arbitrary, D: Arbitrary, E: Arbitrary, G: Arbitrary](
     implicit
     ArbFAB: Arbitrary[F[A, B]],
-    ArbFBC: Arbitrary[F[B, C]],
     ArbFCD: Arbitrary[F[C, D]],
     CogenA: Cogen[A],
     CogenB: Cogen[B],
@@ -22,14 +21,26 @@ trait StrongTests[F[_, _]] extends ProfunctorTests[F] {
     EqFAB: Eq[F[A, B]],
     EqFAD: Eq[F[A, D]],
     EqFAG: Eq[F[A, G]],
-    EqFAEDE: Eq[F[(A, E), (D, E)]],
-    EqFEAED: Eq[F[(E, A), (E, D)]]
+    EqFACBC: Eq[F[(A, C), (B, C)]],
+    EqFDADB: Eq[F[(D, A), (D, B)]],
+    EqFACBD: Eq[F[(A, C), (B, D)]],
+    EqFCADB: Eq[F[(C, A), (D, B)]],
+    EqFACB: Eq[F[(A, C), B]],
+    EqFCAB: Eq[F[(C, A), B]],
+    EqFACDBCD: Eq[F[((A, C), D), ((B, C), D)]],
+    EqFDCADCB: Eq[F[(D, (C, A)), (D, (C, B))]]
   ): RuleSet =
     new DefaultRuleSet(
       name = "strong",
       parent = Some(profunctor[A, B, C, D, E, G]),
-      "strong first distributivity" -> forAll(laws.strongFirstDistributivity[A, B, C, D, E] _),
-      "strong second distributivity" -> forAll(laws.strongSecondDistributivity[A, B, C, D, E] _)
+      "first is swapped second" -> forAll(laws.firstIsSwappedSecond[A, B, C] _),
+      "second is swapped first" -> forAll(laws.secondIsSwappedFirst[A, B, D] _),
+      "lmap equals first and then rmap" -> forAll(laws.lmapEqualsFirstAndThenRmap[A, B, C] _),
+      "lmap equals second and then rmap" -> forAll(laws.lmapEqualsSecondAndThenRmap[A, B, C] _),
+      "dinaturality of first" -> forAll(laws.dinaturalityFirst[A, B, C, D] _),
+      "dinaturality of second" -> forAll(laws.dinaturalitySecond[A, B, C, D] _),
+      "first first is dimap" -> forAll(laws.firstFirstIsDimap[A, B, C, D] _),
+      "second second is dimap" -> forAll(laws.secondSecondIsDimap[A, B, C, D] _)
     )
 }