MonadLogic[StateT[List, A, ?]] violate the "split values" law

[xuwei-k]

Welcome to Scala version 2.11.6 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_25).
Type in expressions to have them evaluated.
Type :help for more information.

scala> import logic._, scalaz._, Scalaz._
import logic._
import scalaz._
import Scalaz._

scala> val M = implicitly[MonadLogic[({type l[a] = StateT[List, Int, a]})#l]]
M: logic.MonadLogic[[a]scalaz.IndexedStateT[[+A]List[A],Int,Int,a]] = logic.MonadLogicInstances1$$anon$2@7eb47a60

scala> val s = StateT[List, Int, Int](s => List((s, s)))
s: scalaz.StateT[List,Int,Int] = scalaz.package$StateT$$anon$1@1b875805

scala> val n = 2
n: Int = 2

scala> val a = M.pure(Option((n, s)))
a: scalaz.IndexedStateT[[+A]List[A],Int,Int,Option[(Int, scalaz.StateT[List,Int,Int])]] = scalaz.package$StateT$$anon$1@4e92dd37

scala> val b = M.split(M.plus(M.pure(n), s))
b: scalaz.IndexedStateT[[+A]List[A],Int,Int,Option[(Int, scalaz.IndexedStateT[[+A]List[A],Int,Int,Int])]] = scalaz.package$StateT$$anon$1@7b97d717

scala> val f = (_: StateT[List, Int, Option[(Int, StateT[List, Int, Int])]]).run(0).map(_.map(_.map(_._2.run(1)))) 
f: scalaz.StateT[List,Int,Option[(Int, scalaz.StateT[List,Int,Int])]] => List[(Int, Option[List[(Int, Int)]])] = <function1>

scala> val x = f(a)
x: List[(Int, Option[List[(Int, Int)]])] = List((0,Some(List((1,1)))))

scala> val y = f(b)
y: List[(Int, Option[List[(Int, Int)]])] = List((0,Some(List((0,0)))))

scala> x === y
res0: Boolean = false

[xuwei-k]

http://hub.darcs.net/dolio/logict/issue/1

Dan DoelOctober 09, 2015
Having looked at the instances, I think this is impossible to fix. The question is whether the WriterT instances should be removed, or the law should be noted as not a law.

treeowlOctober 21, 2016
I believe the law simply isn't a law, at least for now. In particular, the msplit laws only pin down how msplit behaves on values built by "consing" with mplus and mzero. This says an awful lot about [] and I believe also Logic, but much less about other instances. Either the msplit laws need to be strengthened, the reflect law needs to be weakened, or both. I have essentially no intuition whatsoever about what a MonadLogic is supposed to act like, so I have no particular opinion on this as yet.