A backtracking logic programming monad (http://code.haskell.org/~dolio/)

#1MonadLogic WriterT instance don't satisfy reflect law


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)


WriterT [(185471556,[-1449817595]),(-884160399,[0])]
WriterT [(185471556,[-1449817595]),(-884160399,[-1449817595,0])]
  • 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.

  • 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.