Skip to content

Commit

Permalink
Strong profunctor laws based on category theory (typelevel#2640)
Browse files Browse the repository at this point in the history
* add Strong Laws based

* add reference to Notions of Compuations as monoids in StrongLaws

* use new laws in Arrow, CommutativeArrow, ArrowChoice test

* add link to Haskell impl, refactor common parts
  • Loading branch information
lemastero authored and kailuowang committed Feb 15, 2019
1 parent 663f654 commit 2718d5e
Show file tree
Hide file tree
Showing 5 changed files with 80 additions and 22 deletions.
56 changes: 47 additions & 9 deletions laws/src/main/scala/cats/laws/StrongLaws.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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]]],
Expand Down
9 changes: 6 additions & 3 deletions laws/src/main/scala/cats/laws/discipline/ArrowTests.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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]),
Expand Down
21 changes: 16 additions & 5 deletions laws/src/main/scala/cats/laws/discipline/StrongTests.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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],
Expand All @@ -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] _)
)
}

Expand Down

0 comments on commit 2718d5e

Please sign in to comment.