Strong profunctor laws based on category theory #2640

lemastero · 2018-11-25T23:34:21Z

Laws for Strong profunctors were defined in here: #246 but were not based on math foundations.

In paper definition 7.1 of Notions of Computation as Monoids Exequiel Rivas and Mauro Jaskelioff specify 3 laws for profunctor strength.

Based on those Edward Kmett added laws in Haskell Profunctor ekmett/profunctors#38 formulated in terms of first and second and laws that ensure proper definition of first and second

Those laws were recently added to Scalaz: scalaz/scalaz#2028.

This PR proposition to add replace existing laws with those from CT/Haskell/Scalaz:

Laws that ensure proper definition of first and second:

/** 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])

Laws for strength of profunctor (expressed using first):

/** 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 (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))

/** 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)

Above laws for strength of profunctor expressed using second:

/** 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)

/** 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))

/** 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)

WDYT about such change?

codecov-io · 2018-11-26T08:30:18Z

Codecov Report

Merging #2640 into master will increase coverage by 0.26%.
The diff coverage is 100%.

@@            Coverage Diff             @@
##           master    #2640      +/-   ##
==========================================
+ Coverage   94.86%   95.13%   +0.26%     
==========================================
  Files         363      363              
  Lines        6684     6721      +37     
  Branches      283      290       +7     
==========================================
+ Hits         6341     6394      +53     
+ Misses        343      327      -16

Impacted Files	Coverage Δ
.../scala/cats/laws/discipline/ArrowChoiceTests.scala	`100% <ø> (ø)`	⬆️
...c/main/scala/cats/laws/discipline/ArrowTests.scala	`100% <ø> (ø)`	⬆️
...a/cats/laws/discipline/CommutativeArrowTests.scala	`100% <ø> (ø)`	⬆️
.../main/scala/cats/laws/discipline/StrongTests.scala	`100% <100%> (ø)`	⬆️
laws/src/main/scala/cats/laws/StrongLaws.scala	`100% <100%> (ø)`	⬆️
core/src/main/scala/cats/data/ContT.scala	`100% <0%> (ø)`	⬆️
laws/src/main/scala/cats/laws/MonadLaws.scala	`100% <0%> (ø)`	⬆️
core/src/main/scala/cats/data/Ior.scala	`98.54% <0%> (+0.01%)`	⬆️
core/src/main/scala/cats/Eval.scala	`98.82% <0%> (+0.04%)`	⬆️
core/src/main/scala/cats/data/IorT.scala	`97.79% <0%> (+0.04%)`	⬆️
... and 3 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update bf6738e...ee6f128. Read the comment docs.

kailuowang

very nice, Thanks!

ceedubs · 2018-12-03T15:57:31Z

This looks great. Special thanks for documenting the motivation @lemastero!

This looks good to me, but I'm a bit surprised that we aren't getting binary compatibility errors since we have removed some public methods from StrongLaws. Does anyone know why this is the case?

kailuowang · 2018-12-18T15:24:15Z

@ceedubs, we are not testing BC for cats-laws. We never added it to that. I don't think we actually made an official decision on whether to include cats-laws to our BC guarantee, although it might be implied that it is.
Personally, I think there is less need for the BC restriction on cats-laws because:
1, cats-laws is less likely to show up at the root of a diamond dependency graph, since it's mostly used only in tests.
2, also because it's only used in tests, binary incompatibility will only blow up during tests which is much less dangerous.

An extra incentive to break BC in cats-laws is that the Cats ecosystem is stuck on Scalacheck 1.13, because cats-laws maintains BC and wouldn't move to 1.14.

LukaJCB · 2018-12-18T15:52:04Z

I also agree that breaking binary compatability for correctness like this is acceptable 👍

ceedubs · 2018-12-18T16:08:43Z

It sounds like I'm a bit more hesitant than @kailuowang and @LukaJCB to break binary compatibility in cats-laws. Our cats-testkit is based on scalatest, but someone could just as easily write a third-party cats-specs2-testkit or cats-utest-testkit, and breaking binary compatibility would cause issues with those libraries. That is to say, I don't think that we should just think about this in terms of code that's in the test scope and never published.

Lining up versions of scalacheck, discipline and scalatest can already be pretty difficult in a project. I'd hate to add to the complication.

kailuowang · 2018-12-18T16:23:37Z

@ceedubs I agree that breaking BC in cats-laws is not going to be trouble-free. The question is how much trouble and how is that compared to the benefits.
Unlike core I don't see a BC compatible way to change laws, since they are defined in traits.
In the case of cats-specs2-testkit or cats-utest-testkit, I suspect that breaking BC in a specific law would not affect them, but even if it does, their users will find out about it when running tests, rather than blowing up in production. And the fix is simply to update them with the latest cats version (since there shouldn't be many such test libraries (I couldn't find any on github) out there, I'll gladly help upgrading them.

I agree that Scalacheck 1.14 is a different story. Since in that case, we are not at the root.

lemastero · 2018-12-19T13:23:27Z

Thank you for interest in this PR and the insights about BC ❤️
Accepting PR might not be a binary choice though. Some alternatives:

add label/milestone 1.6.0 or 2.0 and merge at the most suitable point in the future
restore existing laws and keep 2 sets of laws for Strong. Existing ones for BC and add strongExt and StrongExtLaws? This is not pretty, but it might be an acceptable compromise.
Reject this PR and live with the laws as they and enjoy full BC.
(It might be fun to explore - how powerful are existing laws :) )

I am working on translating, as much as possible, abstractions from ekmett/profunctors to Scala (in a separated repo). I hope to understand them and share this knowledge. If people find them useful, there will be a compelling reason to move them to cats or somewhere close.

Cheers 🍻

kailuowang · 2018-12-19T14:36:51Z

@lemastero thanks very much for your contribution.
Option 2 is probably still not BC on scala 2.11. We will collect some data from the community regarding cats-laws and we can decide from there.

I would definitely love to see profunctors in the cats ecosystem. Cats-core has very rigid BC restricitions at the moment (for good reason) but I don't see why we shouldn't add this as a separate module, and if you want an independent release cycle, it can be external repo like the other cats external modules like cats-mtl, cats-effect, cats-collections etc.

kailuowang · 2019-02-12T17:08:47Z

@ceedubs binary breaking is no longer a concern because the next release is Cats 2.0 which permits breaking changes for cats-laws and cats-testkit

ceedubs

👍 thanks @lemastero! LGTM

lemastero added 4 commits November 25, 2018 23:32

add Strong Laws based

2d90c65

add reference to Notions of Compuations as monoids in StrongLaws

bae4ccd

use new laws in Arrow, CommutativeArrow, ArrowChoice test

0b133d6

add link to Haskell impl, refactor common parts

ee6f128

kailuowang approved these changes Nov 27, 2018

View reviewed changes

kailuowang added the Binary Breaking label Jan 12, 2019

kailuowang added this to the 2.0 milestone Feb 5, 2019

kailuowang requested a review from ceedubs February 12, 2019 17:07

ceedubs approved these changes Feb 15, 2019

View reviewed changes

kailuowang merged commit 2718d5e into typelevel:master Feb 15, 2019

kailuowang added the testing label Feb 15, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Strong profunctor laws based on category theory #2640

Strong profunctor laws based on category theory #2640

lemastero commented Nov 25, 2018 •

edited

Loading

codecov-io commented Nov 26, 2018 •

edited

Loading

kailuowang left a comment

ceedubs commented Dec 3, 2018

kailuowang commented Dec 18, 2018

LukaJCB commented Dec 18, 2018

ceedubs commented Dec 18, 2018

kailuowang commented Dec 18, 2018 •

edited

Loading

lemastero commented Dec 19, 2018

kailuowang commented Dec 19, 2018

kailuowang commented Feb 12, 2019

ceedubs left a comment

Strong profunctor laws based on category theory #2640

Strong profunctor laws based on category theory #2640

Conversation

lemastero commented Nov 25, 2018 • edited Loading

codecov-io commented Nov 26, 2018 • edited Loading

Codecov Report

kailuowang left a comment

Choose a reason for hiding this comment

ceedubs commented Dec 3, 2018

kailuowang commented Dec 18, 2018

LukaJCB commented Dec 18, 2018

ceedubs commented Dec 18, 2018

kailuowang commented Dec 18, 2018 • edited Loading

lemastero commented Dec 19, 2018

kailuowang commented Dec 19, 2018

kailuowang commented Feb 12, 2019

ceedubs left a comment

Choose a reason for hiding this comment

lemastero commented Nov 25, 2018 •

edited

Loading

codecov-io commented Nov 26, 2018 •

edited

Loading

kailuowang commented Dec 18, 2018 •

edited

Loading