Logic does not commute!

As if it hasn't been hammered home enough: monads don't commute. But what does that mean, practically? Most of the well-behaved ones like Reader, State, Writer, Maybe, and Except kind of work when you change them around (though you will find things like StateT s (Except e) and ExceptT e (State s) to have distinct flavors). However, some monads are so weird that rearranging them doesn't do anything close to what you think they should do. It's too easy to break scoped effects like local (via Reader) if you compose the wrong way with Logic. (I think the same holds true for any list transformer.) Here's an example:

module NoCommute where

import Control.Monad.Logic (Logic, LogicT (..), MonadLogic (..),
  observeAll, observeAllT, observeMany, observeManyT)
import Control.Monad.Reader (Reader, ReaderT (..), MonadReader (..), runReader)
import Control.Applicative (Alternative (..))
import Data.List (unfoldr)

-- | Search monad with reader on the outside and logic on the inside
newtype RL r a = RL { unRL :: ReaderT r Logic a }
  deriving newtype (Functor, Applicative, Monad,
    Alternative, MonadLogic, MonadReader r)

-- | Compute all results at once
runRL :: RL r a -> r -> [a]
runRL m r = observeAll (runReaderT (unRL m) r)

unconsRL :: RL r a -> r -> Maybe (a, RL r a)
unconsRL m r =
  case observeMany 1 (runReaderT (unRL (msplit m)) r) of
    [] -> Nothing
    ma : _ -> ma

-- | Compute results incrementally
unfoldRL :: RL r a -> r -> [a]
unfoldRL mStart r = unfoldr (`unconsRL` r) mStart

-- | Search monad with logic on the outside and reader on the inside
newtype LR r a = LR { unLR :: LogicT (Reader r) a }
  deriving newtype (Functor, Applicative, Monad,
    Alternative, MonadLogic, MonadReader r)

runLR :: LR r a -> r -> [a]
runLR m r = runReader (observeAllT (unLR m)) r

unconsLR :: LR r a -> r -> Maybe (a, LR r a)
unconsLR m r = case runReader (observeManyT 1 (unLR (msplit m))) r of
  [] -> Nothing
  ma : _ -> ma

unfoldLR :: LR r a -> r -> [a]
unfoldLR mStart r = unfoldr (`unconsLR` r) mStart

-- | A simple test: increment a local counter and yield it twice
test :: (MonadReader Int m, Alternative m) => m Int
test = local (+1) (ask <|> ask)

-- | Results:
-- RL run    [1,1]
-- RL unfold [1,1]
-- LR run    [1,0]
-- LR unfold [1,0]
runTest :: IO ()
runTest = do
  putStr "RL run    "
  print (runRL test 0)
  putStr "RL unfold "
  print (unfoldRL test 0)
  putStr "LR run    "
  print (runLR test 0)
  putStr "LR unfold "
  print (unfoldLR test 0)

RL behaves well, with each branch observing the environment under the local (+1) scope, but I can't justify the behavior of LR. The first result is scoped, but the second resumes with the original environment. If it yields such unintuitive behavior as this, I think the MonadReader instance for LogicT should be removed altogether.

I'm sure there are papers to read about the weirdness of effects with scoping constructs...