MMonad expectations

[treeowl]

Is the argument to embed expected to be a monad morphism? I'm guessing so? I believe that having only a Monad n constraint, and not a Monad m one, makes it impossible to write sensible instances for reflection-without-remorse-style logic monads without that restriction.

[treeowl]

Specifically, I'm thinking of the new logict-sequence. With Monad m and Monad n constraints, we could write

embedSeq :: (Monad m, Monad n) => (forall a. m a -> SeqT n a) -> SeqT m a -> SeqT n a
embedSeq f s = f (toView s) >>= \r -> case r of
  Empty -> empty
  a :< s' -> pure a <|> embedSeq f s'

where toView requires a Monad constraint. Lawful? I haven't checked, but I have a good feeling about it, and it's guaranteed to at least respect == when passed an arbitrary function.

Without that, following the types leads to this monstrosity:

instance MMonad SeqT where
  embed (f :: forall a. m a -> SeqT n a) (SeqT m0) = SeqT $ fmap go m0
    where
      go :: forall b. m (View m b) -> n (View n b)
      go m = toView (f m) >>= \r -> case r of
        Empty -> pure Empty
        Empty :< s -> toView (step s)
        (x :< q) :< s -> pure $ x :< (embed f q <|> step s)

      step :: forall b. SeqT n (View m b) -> SeqT n b
      step s = s >>= \r -> case r of
        Empty -> empty
        a :< s' -> pure a <|> embed f s'

Lawful? Couldn't begin to guess. And very unlikely to be at all well-behaved if the function is not a monad morphism.

[turion]

How does your instance MMonad SeqT avoid having a Monad n constraint? You're using >>= in step, for example, but Monad (SeqT n) requires Monad n.

[turion]

There is a similar issue about ProgramT, which uses a view function which needs a Monad constraint: https://github.com/Gabriel439/Haskell-MMorph-Library/issues/11#issuecomment-847125948 But if you dig down into the definition of ProgramT, you can implement the instance directly without using the view function. Maybe it's similar here, but it would also lead to a more complicated instance than the one defined via toView.

[treeowl]

How does your instance MMonad SeqT avoid having a Monad n constraint? You're using >>= in step, for example, but Monad (SeqT n) requires Monad n.

I don't avoid a Monad n constraint. I avoid a Monad m constraint, which is sufficient for embed. Yes, hoist and embed do that differently! How awful. My most urgent question is about the documentation of the class, but I think Gabriel already knows I favor putting both constraints on.

[turion]

Ohh, thanks for the clarification. Yes, this is quite confusing.

Regarding your original question, I sometimes use transformers as Applicative transformers, and there I usually don't expect the natural transformations to be monad morphisms.

Is there a case of an MMonad instance where one has to count on the monad morphism laws to prove the MMonad laws?

[treeowl]

Well, for the complicated instance I gave, I'd be surprised if embed even respected equality if passed an arbitrary function. Take a simpler example:

newtype Boom m a = Boom
  (m (Maybe a, Boom m a))
newtype Bang m a = Bang
  (m (a, Bang m a))
boomBang :: Monad m => Boom m a -> Bang m a
boomBang (Boom m) = Bang $ m >>= \case
  (Nothing, b) -> boomBang b
  (Just a, m') -> (a, boomBang b)

Imagine we consider Boom a representation of Bang, so b == c = True iff boomBang b == boomBang c. Now if you hoist or embed something over Boom that's not a monad morphism, I don't think you'll respect ==.

[treeowl]

Unless, that is, you convert the Boom stepwise into something Bang-like, which requires a Monad instance for the original monad.