StateT violates laws

[ceedubs]

As pointed out here

This reveals law violations in StateT. It looks like flatMap/ap
consistency does not hold, as well as MonadCombine
right-distributivity. It's not immediately clear to me how to fix this,
so I'm opening this up in case somebody else gets to it first.

[ceedubs]

cc @djspiewak @edmundnoble

[kailuowang]

ouch

[djspiewak]

@ceedubs Just to short-circuit some work, I assume you found the inconsistency issues in flatMap/ap when you tried to fix the Arbitrary to be more comprehensive. Can you paste the revised Arbitrary?

[djspiewak]

@ceedubs Oh, I can't read. I thought this was an issue, not a PR. :-P

[kailuowang]

to save a trip to the CI to get the actual error message:

[info] - StateT[ListWrapper, Int, Int].monadState.flatMap consistent apply *** FAILED ***
[info] GeneratorDrivenPropertyCheckFailedException was thrown during property evaluation.
[info] (Discipline.scala:14)
[info] Falsified after 4 successful property evaluations.
[info] Location: (Discipline.scala:14)
[info] Occurred when passed generated values (
[info] arg0 = cats.data.StateT@8,
[info] arg1 = cats.data.StateT@9
[info] )
[info] Label of failing property:
[info] (cats.data.StateT@6 ?== cats.data.StateT@7) failed

[info] - StateT[ListWrapper, Int, Int].monad.flatMap consistent apply *** FAILED ***
[info] GeneratorDrivenPropertyCheckFailedException was thrown during property evaluation.
[info] (Discipline.scala:14)
[info] Falsified after 4 successful property evaluations.
[info] Location: (Discipline.scala:14)
[info] Occurred when passed generated values (
[info] arg0 = cats.data.StateT@c,
[info] arg1 = cats.data.StateT@d
[info] )
[info] Label of failing property:
[info] (cats.data.StateT@a ?== cats.data.StateT@b) failed

I probably missed something but I didn't find error for MonadCombine right-distributivity for StateT though.

[kailuowang]

found it, apparently MonadCombine right distributivity is only failing on JVM builds, passing on JS builds.

• StateT[ListWrapper, Int, Int].monadCombine.right distributivity *** FAILED *** (5 milliseconds)
  [info] GeneratorDrivenPropertyCheckFailedException was thrown during property evaluation.
  [info] (Discipline.scala:14)
  [info] Falsified after 11 successful property evaluations.
  [info] Location: (Discipline.scala:14)
  [info] Occurred when passed generated values (
  [info] arg0 = cats.data.StateT@7264447,
  [info] arg1 = cats.data.StateT@614c94fb,
  [info] arg2 = cats.data.StateT@6ac91ca4
  [info] )
  [info] Label of failing property:
  [info] (cats.data.StateT@3d8628f7 ?== cats.data.StateT@32eb8faf) failed
  [info] org.scalatest.exceptions.GeneratorDrivenPropertyCheckFailedException:
  [info] at org.scalatest.enablers.CheckerAsserting$$anon$2.indicateFailure(CheckerAsserting.scala:223)
  [info] at org.scalatest.enablers.CheckerAsserting$$anon$2.indicateFailure(CheckerAsserting.scala:219)
  [info] at org.scalatest.enablers.UnitCheckerAsserting$CheckerAssertingImpl.check(CheckerAsserting.scala:116)
  [info] at org.scalatest.prop.Checkers$class.check(Checkers.scala:374)
  [info] at cats.tests.StateTTests.check(StateTTests.scala:11)
  [info] at org.typelevel.discipline.scalatest.Discipline$$anonfun$checkAll$2$$anonfun$apply$1.apply(Discipline.scala:14)
  [info] at org.typelevel.discipline.scalatest.Discipline$$anonfun$checkAll$2$$anonfun$apply$1.apply(Discipline.scala:14)
  [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85)
  [info] at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
  [info] at org.scalatest.Transformer.apply(Transformer.scala:22)
  [info] at org.scalatest.Transformer.apply(Transformer.scala:20)
  [info] at org.scalatest.FunSuiteLike$$anon$1.apply(FunSuiteLike.scala:186)
  [info] at org.scalatest.TestSuite$class.withFixture(TestSuite.scala:196)
  [info] at org.scalatest.FunSuite.withFixture(FunSuite.scala:1560)
  [info] at org.scalatest.FunSuiteLike$class.invokeWithFixture$1(FunSuiteLike.scala:183)
  [info] at org.scalatest.FunSuiteLike$$anonfun$runTest$1.apply(FunSuiteLike.scala:196)
  [info] at org.scalatest.FunSuiteLike$$anonfun$runTest$1.apply(FunSuiteLike.scala:196)
  [info] at org.scalatest.SuperEngine.runTestImpl(Engine.scala:289)
  [info] at org.scalatest.FunSuiteLike$class.runTest(FunSuiteLike.scala:196)
  [info] at org.scalatest.FunSuite.runTest(FunSuite.scala:1560)
  [info] at org.scalatest.FunSuiteLike$$anonfun$runTests$1.apply(FunSuiteLike.scala:229)
  [info] at org.scalatest.FunSuiteLike$$anonfun$runTests$1.apply(FunSuiteLike.scala:229)
  [info] at org.scalatest.SuperEngine$$anonfun$traverseSubNodes$1$1.apply(Engine.scala:396)
  [info] at org.scalatest.SuperEngine$$anonfun$traverseSubNodes$1$1.apply(Engine.scala:384)
  [info] at scala.collection.immutable.List.foreach(List.scala:392)
  [info] at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:384)
  [info] at org.scalatest.SuperEngine.org$scalatest$SuperEngine$$runTestsInBranch(Engine.scala:379)
  [info] at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:461)
  [info] at org.scalatest.FunSuiteLike$class.runTests(FunSuiteLike.scala:229)
  [info] at org.scalatest.FunSuite.runTests(FunSuite.scala:1560)
  [info] at org.scalatest.Suite$class.run(Suite.scala:1147)
  [info] at org.scalatest.FunSuite.org$scalatest$FunSuiteLike$$super$run(FunSuite.scala:1560)
  [info] at org.scalatest.FunSuiteLike$$anonfun$run$1.apply(FunSuiteLike.scala:233)
  [info] at org.scalatest.FunSuiteLike$$anonfun$run$1.apply(FunSuiteLike.scala:233)
  [info] at org.scalatest.SuperEngine.runImpl(Engine.scala:521)
  [info] at org.scalatest.FunSuiteLike$class.run(FunSuiteLike.scala:233)
  [info] at org.scalatest.FunSuite.run(FunSuite.scala:1560)
  [info] at org.scalatest.tools.Framework.org$scalatest$tools$Framework$$runSuite(Framework.scala:314)
  [info] at org.scalatest.tools.Framework$ScalaTestTask.execute(Framework.scala:480)
  [info] at sbt.TestRunner.runTest$1(TestFramework.scala:76)
  [info] at sbt.TestRunner.run(TestFramework.scala:85)
  [info] at sbt.TestFramework$$anon$2$$anonfun$$init$$1$$anonfun$apply$8.apply(TestFramework.scala:202)
  [info] at sbt.TestFramework$$anon$2$$anonfun$$init$$1$$anonfun$apply$8.apply(TestFramework.scala:202)
  [info] at sbt.TestFramework$.sbt$TestFramework$$withContextLoader(TestFramework.scala:185)
  [info] at sbt.TestFramework$$anon$2$$anonfun$$init$$1.apply(TestFramework.scala:202)
  [info] at sbt.TestFramework$$anon$2$$anonfun$$init$$1.apply(TestFramework.scala:202)
  [info] at sbt.TestFunction.apply(TestFramework.scala:207)
  [info] at sbt.Tests$.sbt$Tests$$processRunnable$1(Tests.scala:239)
  [info] at sbt.Tests$$anonfun$makeSerial$1.apply(Tests.scala:245)
  [info] at sbt.Tests$$anonfun$makeSerial$1.apply(Tests.scala:245)
  [info] at sbt.std.Transform$$anon$3$$anonfun$apply$2.apply(System.scala:44)
  [info] at sbt.std.Transform$$anon$3$$anonfun$apply$2.apply(System.scala:44)
  [info] at sbt.std.Transform$$anon$4.work(System.scala:63)
  [info] at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:228)
  [info] at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:228)
  [info] at sbt.ErrorHandling$.wideConvert(ErrorHandling.scala:17)
  [info] at sbt.Execute.work(Execute.scala:237)
  [info] at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:228)
  [info] at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:228)
  [info] at sbt.ConcurrentRestrictions$$anon$4$$anonfun$1.apply(ConcurrentRestrictions.scala:159)
  [info] at sbt.CompletionService$$anon$2.call(CompletionService.scala:28)
  [info] at java.util.concurrent.FutureTask.run(FutureTask.java:262)
  [info] at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:471)
  [info] at java.util.concurrent.FutureTask.run(FutureTask.java:262)
  [info] at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1145)
  [info] at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:615)
  [info] at java.lang.Thread.run(Thread.java:745)

[djspiewak]

I'm pretty sure I know what's going on here. StateT is fundamentally a monad composed with itself, and some of the functions (e.g. flatMap and map2) actually take advantage of this by defining themselves in terms of the underlying FlatMap and Applicative (as relevant) instances. Unfortunately, as we know, this isn't sound in general, even if the types say it should be. All of the laws are tested with ListWrapper, and as a non-commutive monad, List is one of the best exemplars of where this sort of technique breaks down.

tl;dr: I don't think it's sound to define StateT as F[S => F[(S, A)]], and I think the revised Arbitrary is revealing legitimate issues.

[ceedubs]

@djspiewak Sorry I haven't had a chance to come back to this, but what you are saying is what I was fearing might be the case. I'm not sure how to proceed. I remember that some time back @TomasMikula had a POC of a stack-safe State that maintained an internal heap-based composition of functions (similarly to the encoding of Free) that looked promising. I'm wondering if something like that might be better and might also help with issues such as #107 (comment). However that approach might break down with StateT.

[djspiewak]

Here's a slightly more rigorous treatment of my intuition from earlier…

1. Define: forall f s a . StateT f s a = f $ s -> f (s, a)
2. Let s = ()
3. f $ () -> f ((), a) simplifies to f $ f a
4. We're attempting to define Monad for this construct, but f $ f a is literally just ComposedMonad f f, which is unsound (see discussion on Proof of concept of ComposedMonad #1478)
5. Thus, we have a counter-example instance of s which demonstrates that the overall formulation is not sound in general

[djspiewak]

@ceedubs I'll look into the reformulation. Shouldn't be too hard, I think, and I doubt it will break down with StateT. The biggest danger is making sure that it composes with the intuitive semantics over non-algebraic instances f (such as Cont, but also List and other troublemakers).

[edmundnoble]

I wonder if another way to fix this might be to hide the representation from the user, and just make the constructors consistent.

Edit: How does it make sense that StateT not being a monad would break the ap/flatMap consistency law, and not the flatMap associativity law? It sounds to me like we have an incorrect implementation of ap.

[djspiewak]

An update on this: I spent some time talking with @jdegoes about the issue last week, and some playing around with strawmen convinced me that I overgeneralized the problem a bit. We definitely can't override map2 in the fashion done here, and in retrospect it's relatively obvious why that is problematic, but there's no evidence at present that the construct is fundamentally broken.

Critically, all of the "nested monad" breaking examples (notably, from @TomasMikula and the classic Haskell ListT counter-examples) lean on traverse. Something I didn't realize, which really should be broadcast more widely, is the fact that Haskell's ListT >>= implementation delegates to mapN, rather than the intuitive (and correct!) nested >>=. mapN is, of course, implemented by Traverse on [], which is the main reason why ListT is broken. None of these examples apply to a monad nested with itself, which is a construct that I tried pretty hard to break and couldn't (it's weird, but not unlawful so far as I can contrive).

At any rate…  Still pushing on this. We'll see where it leads.