Weaken hoist constraint

[treeowl]

As discussed in this SO post, the Monad m constraint on hoist feels too strong in the face of hoist id = id. Cirdec thinks it probably should be Functor. I don't know if anything could legitimately use Applicative.

[Gabriella439]

Yes, it should be Functor. The original reason for the more restrictive Monad constraint was that back when Functor was not a super-class of Monad I wanted to simplify constraints by not having to specify (Functor m, Monad m) in several places. My rule of thumb is that once Debian stable switches to ghc-7.10 then I will update this to use the weaker Functor constraint (and bump the major number to 1.1 since that would be a breaking API change).

[isovector]

I have a use case for the relaxed constraints on hoist also. It's not immediately obvious why Debian's release process should influence this module. If it really is, a github release that we could target with stack would be greatly appreciated.

[Gabriella439]

Alright, this is up on Hackage as mmorph-1.0.7. I realized that I could do this using CPP and still maintain compatibility with older ghc versions

[hvr]

turns out compatibility via CPP was not maintained, see #31 for more details

[treeowl]

@Gabriel439 since the change closing this ticket was reverted (it really shouldn't have been made in a minor release), can we reopen this ticket to consider making the change in the next major release?

[Gabriella439]

@treeowl: @snoyberg noted in https://github.com/Gabriel439/Haskell-MMorph-Library/issues/31 that conduit uses the stronger Monad constraint for its MFunctor instance for efficiency reasons. See https://hackage.haskell.org/package/conduit-1.2.10/docs/src/Data-Conduit-Internal-Conduit.html#line-142

[treeowl]

@Gabriel439, @snoyberg: the implementation of hoist for ConduitM contains the following comment:

Combine a series of monadic actions into a single action. Since we throw away side effects between different actions, an arbitrary break between actions will lead to a violation of the monad transformer laws. Example available at:

http://hpaste.org/75520

The part of the code that comment refers to is the very part that requires a Monad m constraint on hoist. So my view is that the use should not be supported, conduit should change its MFunctor instance, and conduit users should use transPipe when they want the collapsing optimization.

Whether the type change should be re-instituted is a different judgement call altogether. I still don't actually know if there are legitimate MFunctor instances that can't be generalized! If you decide to leave MFunctor as it is, perhaps it would make sense to add

class MFunctor t => FFunctor t where
  foist :: Functor f => (forall a. f a -> g a) -> t f b -> t g b

[Gabriella439]

I'll reopen with the goal of eventually making the constraint switch to Functor as a breaking change, but I'd like to first migrate downstream libraries on Hackage before making the change to avoid disruption

[treeowl]

I think we should consider the mathematics of the thing (which I don't know much about myself). MFunctor is supposed to be a functor in the category of Monads. For that purpose, the obvious signature is

class MFunctor t where
  hoist :: (Monad m, Monad n) => (forall a. m a -> n a) -> t m b -> t n b

The current signature calls for only a constraint on m, which is sufficient for the current instances. Is there a deep reason for that? Would it be possible to come up with a legitimate functor t that needs a Functor n constraint? Furthermore, as discussed, the current known-to-me legitimate instances only require a Functor constraint, rather than a Monad one. Is there a reason for that? If we really only will ever need Functor m, then yes, we should go for it. But if there are potential cases where we may want more, we should tread carefully.

[treeowl]

Oh, silly me. I forgot my original reasoning from the SO post! Since hoist id = id, we're practically prohibited from using join, I believe. So that immediately weakens the constraint to Functor. And it's hard to imagine needing the Functor instance for anything other than applying the given function under m, which we can do in either order. So yeah, weakening the constraint seems pretty reasonable. If there are situations where collapsing is semantically okay and also actually useful, maybe it would make sense to instead add a foist method to MFunctor, giving a default definition of hoist = foist.

[Gabriella439]

So actually, conduit is not the only library that uses the Monad constraint. I forgot that my own pipes library does, too, and I'll explain why.

Semantically the Proxy type is a free monad transformer and could be implemented as:

data ProxyF a' a b' b x = Request a' (a -> x) | Response b (b' -> x)

type Proxy a' a b' b = FreeT (ProxyF a' a b' b)

... but under the hood it uses a more efficient internal representation that can be used to violate the monad morphism laws for MonadTrans. The public facing API (including the MFunctor instance for Proxy) has to take care to not expose a way to violate these monad morphism laws.

The implementation of hoist uses the Monad constraint to insert returns to protect the internal representation in this way

So pipes could implement a law-abiding hoist (in fact, the implementation of hoist would get much faster if it did so and that is how unsafeHoist is implemented) but it would come at the price of efficiency elsewhere because the internal representation would need to insert a mandatory layer of the base monad before every step of the Proxy in order to preserve correctness of the public API

[treeowl]

I read your notes in the source, and I don't understand the problem. If I read it correctly (which I certainly may not have), the law violation can only be observed by pattern matching on the Proxy constructors. Since those are "internal", wouldn't it make more sense to define hoist = unsafeHoist and offer a safeHoist for people messing with internals? Or is there a more severe law violation capable of leaking through the "public" interface?

On May 19, 2017 11:14 AM, "Gabriel Gonzalez" notifications@github.com wrote:

So actually, conduit is not the only library that uses the Monad constraint. I forgot that my own pipes library does, too, and I'll explain why.

Semantically the Proxy type is a free monad transformer and could be implemented as:

data ProxyF a' a b' b x = Request a' (a -> x) | Response b (b' -> x) type Proxy a' a b' b = FreeT (ProxyF a' a b' b)

... but under the hood it uses a more efficient internal representation that can be used to violate the monad morphism laws for MonadTrans. The public facing API (including the MFunctor instance for Proxy) has to take care to not expose a way to violate these monad morphism laws.

The implementation of hoist uses the Monad constraint to insert returns to protect the internal representation in this way

So pipes could implement a law-abiding hoist (in fact, the implementation of hoist would get much faster if it did so and that is how unsafeHoist is implemented) but it would come at the price of efficiency elsewhere because the internal representation would need to insert a mandatory layer of the base monad before every step of the Proxy in order to preserve correctness of the public API

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/Gabriel439/Haskell-MMorph-Library/issues/28#issuecomment-302730374, or mute the thread https://github.com/notifications/unsubscribe-auth/ABzi_WZwvRTQL5lZSoeglvnLOU1cENbIks5r7bHHgaJpZM4KRpnq .

[treeowl]

I think the thing to do is to get much more explicit about what it means for two pipes to be equivalent. Here's my recommendation for doing so:

module Pipes.Step where

import qualified Pipes.Internal as P
import Pipes.Internal (Proxy)

data Step a' a b' b m r
    = Request a' (a  -> Proxy a' a b' b m r )
    | Respond b  (b' -> Proxy a' a b' b m r )
    | Pure    r

-- | Run a 'Proxy' one step and then stop.
step :: Monad m
     => Proxy a' a b' b m r
     -> m (Step a' a b' b m r)
step (P.Request a' f) = pure (Request a' f)
step (P.Respond b g) = pure (Respond b g)
step (P.Pure r) = pure (Pure r)
step (P.M m) = m >>= step

-- | Convert a 'Step' into a 'Proxy'
wrapStep :: Step a' a b' b m r -> Proxy a' a b' b m r
wrapStep (Request a' f) = P.Request a' f
wrapStep (Respond b g) = P.Respond b g
wrapStep (Pure r) = P.Pure r

The key idea is that we can (coinductively, I guess) define proxies p and q as equivalent if and only if step p is equivalent to step q. Two steps, in turn, are equivalent if they're built from the same constructor and, when it's a Request or Response, have the same request/response and (coinductively, again) equivalent callbacks.

Here's a proof of the monad transformer laws under this equivalence (I hope I got this right):

lift . return === return:

  step (lift (return a))
= step (M (return a >>= \r -> return (Pure r)))
= step (M (return (Pure a)))
= return (Pure a) >>= step
= step (Pure a)
= step (return a)

lift (m >>= f) === lift m >>= lift . f:

  step (lift (m >>= f)
= step (M ((m >>= f) >>= \r -> return (Pure r)))
= step (M (m >>= \a -> f a >>= \r -> return (Pure r)))
= (m >>= \a -> f a >>= \r -> return (Pure r)) >>= step
= m >>= \a -> f a >>= \r -> step (Pure r)
= m >>= \a -> f a >>= \r -> pure (S.Pure r)
-- Sorry for the alpha conversion
= m >>= \r -> f r >>= \r' -> pure (S.Pure r')
= m >>= \r -> f r >>= \r' -> step (Pure r')
= m >>= \r -> (f r >>= \r' -> return (Pure r')) >>= step
= m >>= \r -> step (M (f r >>= \r' -> return (Pure r')))
= m >>= \r -> step (lift (f r))
= m >>= \r -> step (Pure r >>= lift . f)
= ((m >>= \r -> return (Pure r)) >>= \p' -> return (p' >>= lift . f)) >>= step
= step (M ((m >>= \r -> return (Pure r)) >>= \p' -> return (p' >>= lift . f)))
= step (M (m >>= \r -> return (Pure r)) >>= lift . f)
= step (lift m >>= lift . f)

[treeowl]

Oh, I should mention a couple things

Why step?

The Step type is very similar to the free monad transformer you described, except that it corecursively uses Proxy. It's possible to implement a few key functions in terms of step and wrapStep, which I think are likely sufficient to justify using it in this fashion:

runEffect p = do
  s <- step p
  case s of
    Request x _ -> absurd x
    Respond _ g -> runEffect (g ())
    Pure r -> pure r

push a = wrapStep $ Respond a (\a' -> wrapStep $ Request a' push)
pull a' = wrapStep $ Request a' (\a -> wrapStep $ Respond a pull)
request a' = wrapStep $ Request a' (wrapStep . Pure)
respond a = wrapStep $ Respond a (wrapStep . Pure)

What, really, is the problem with unsafeHoist?

I still don't see the problem with unsafeHoist, even under strict equality. Can you explain exactly what you're preventing and how?

[Gabriella439]

pipes already defines such an equivalence, which that Proxys are equivalent if they are identical when viewed through the observe function. See: https://hackage.haskell.org/package/pipes-4.3.3/docs/Pipes-Internal.html#v:observe

However, that doesn't fix the underlying problem, which is that I don't want users of my public API to have to understand that equivalence to use the library correctly. I want the public API to absolutely forbid misuse of the library in any way while sacrificing as little performance as possible.

[Gabriella439]

The problem with unsafeHoist specifically is that it lets you detect violations of the monad morphism laws for lift if you pass an argument that is not a monad morphism. For example:

example :: Monad m => m a -> WriterT (Sum Int) m a
example m = do
    tell (Sum 1)
    m

-- You can use this to count how many `M` layers there are in a `Proxy`:
unsafeHoist example
    :: Monad m => Proxy a' a b' b m r -> Proxy a' a b' b (WriterT (Sum Int) m) r

-- ... which allows you to detect a violation of the monad transformer laws for `lift`:
unsafeHoist example (return x) /= unsafeHoist example (lift (return x))

[duog]

I think we should consider the mathematics of the thing (which I don't know much about myself). MFunctor is supposed to be a functor in the category of Monads. For that purpose, the obvious signature is

class MFunctor t where hoist :: (Monad m, Monad n) => (forall a. m a -> n a) -> t m b -> t n b The current signature calls for only a constraint on m, which is sufficient for the current instances. Is there a deep reason for that? Would it be possible to come up with a legitimate functor t that needs a Functor n constraint? Furthermore, as discussed, the current known-to-me legitimate instances only require a Functor constraint, rather than a Monad one. Is there a reason for that? If we really only will ever need Functor m, then yes, we should go for it. But if there are potential cases where we may want more, we should tread carefully.

The types Control.Monad.Trans.FreeT and Control.Monad.Trans.Church.FT from free seem like they should be able to have valid instances of MFunctor, with hoist = hoistFreeT and hoist = hoistFT. hoistFreeT requires Monad m, but only uses liftM, so would not pose a problem. However, hoistFT does seem to require Monad n.

[neongreen]

The current signature calls for only a constraint on m, which is sufficient for the current instances. Is there a deep reason for that?

@Gabriel439 so is it true that there's no Monad n constaint in hoist simply because there wasn't a need for it, or are there any other reasons?

[Gabriella439]

The original reason was mainly to minimize necessary constraints

However, later on the code in Control.Monad.Trans.Compose came to depend on the smaller constraint. I believe if you add the Monad n constraint to hoist then that module no longer compiles (and is not easy to fix)

[qrpnxz]

I tried to add the constraint, and indeed ComposeT doesn't like it. Problem is that MonadTrans is not required to be Monad... until transformers version 0.6.0.0 that is. But I don't have that version on my system, and I realized that the way I was trying to implement the instance that required Monad didn't respect hoist id = id anyway. 😄 Can't forget about the laws.