hub.darcs.net :: dolio -> logict -> issue

#1MonadLogic WriterT instance don't satisfy reflect law

pocketberserker

code:

import Control.Monad
import Control.Monad.Writer.Strict
import Control.Monad.Logic
 
hoge :: WriterT [Int] [] Int
hoge = WriterT $ [ (185471556, [-1449817595]) ]
 
fuga :: WriterT [Int] [] Int
fuga = WriterT $ [ (-884160399, [0]) ]
 
piyo :: WriterT [Int] [] Int
piyo = hoge `mplus` fuga
 
main = do
  print piyo
  print $ (msplit piyo >>= reflect)

output:

WriterT [(185471556,[-1449817595]),(-884160399,[0])]
WriterT [(185471556,[-1449817595]),(-884160399,[-1449817595,0])]

• Dan DoelFri Oct 9 01:26:48 UTC 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.

• treeowlFri Oct 21 04:06:39 UTC 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.