Why is the n of hoist not a monad?

[nikita-volkov]

I mean, why

hoist :: Monad m => (forall a. m a -> n a) -> t m b -> t n b

instead of

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

?

I've stumbled upon that trying to implement MMonad in terms of this function.

[Gabriella439]

See this StackOverflow question and answer, which explain the rationale behind this.

The quick summary is: this keeps constraints smaller and I haven't (yet) encountered an instance that required the Monad n constraint.

[nikita-volkov]

I haven't (yet) encountered an instance that required the Monad n constraint.

Well, you have one now.

I must note that the alternative MonadTransFunctor of the "layers" package, accepted that function just fine.

[Gabriella439]

instance MFunctor Deserialize where
    hoist nat (Deserialize k) = Deserialize (nat . liftM (hoist nat) . k)

instance MFunctor Result where
    hoist nat (Fail str bs) = Fail str bs
    hoist nat (Partial k)   = Partial (nat . liftM (hoist nat) . k)
    hoist nat (Done a bs)   = Done a bs

[nikita-volkov]

Wow! Tunnel vision... Okay thanks.

[Gabriella439]

No problem at all! :)

[ghost]

Here's another example:

type f ⥴ g = ∀ a. f a → g a

unViewTransT
  ∷ ∀ instr f g α.
    ( Monad f
    , Monad g
    )
  ⇒ (f ⥴ g)
  → f (ProgramViewT instr f α)
  → ProgramT instr g α
unViewTransT η = join ∘ lift ∘ η ∘ (return ∘ go =≪)
  where
    go ∷ ProgramViewT instr f α → ProgramT instr g α
    go (m :>>= k) = singleton m ≫= unViewTransT η ∘ viewT ∘ k
    go (Return a) = return a

hoist
  ∷ ( Monad f
    , Monad g
    )
  ⇒ (f ⥴ g)
  → (ProgramT instr) f β
  → (ProgramT instr) g β
hoist η = unViewTransT η ∘ viewT

I don't see another way to do this since ProgramT is abstract.

[Gabriella439]

I tried my hand at this, and I don't think it's possible unless operational exposes an unViewT operation that is the inverse of viewT. However, it seems like the operational library could add this instance using the internals quite easily.

[ghost]

Thanks for looking at this. Indeed, the main difficulty here seems to be that the internals of ProgramT are abstract and the only way to put things back is through the Monad instance.

I saw your comment about wanting to minimize constraints. I'm curious though, have you found many cases where requiring a Monad instance for the codomain actually causes a problem rather than perhaps just being inconvenient? It seems a bit problematic if the internal representation of the monad must be accessible (or we get lucky and the author provide the necessary machinery like unViewT) in order to be able to define MFunctor.

[Gabriella439]

Well, in this case I don't mind relying on it having access to the internal representation since it would be an orphan instance otherwise. However, even without that internal access, it still makes sense for operational to provide an unViewT operation that doesn't require a Monad constraint. I interpret this particular issue as highlighting the need for unViewT.

[ghost]

Good point. I suppose the desire to avoid orphan instances does make this more of an issue for the library author… And I agree that an inverse to viewT should be provided. I was a bit surprised it wasn't there already.

[treeowl]

Here's another one: the free package defines

hoistFT :: (Monad m, Monad n) => (forall a. m a -> n a) -> FT f m b -> FT f n b
hoistFT phi (FT m) = FT (\kp kf -> join . phi $ m (return . kp) (\xg -> return . kf (join . phi . xg)))

If there's a way to weaken that to Monad m, I haven't been able to find it. I suspect the "work from the inside out" approach may be defeated by this Yoneda-style type.

[Gabriella439]

@treeowl: Yeah, for the efficient implementation you require the Monad n constraint. In theory you can still do it inefficiently by converting to Control.Monad.Trans.Free.FreeT and then converting back

The problem is that adding the Monad n constraint breaks the Control.Monad.Trans.Compose module

[treeowl]

I don't think you can convert back.

…

On May 21, 2017 10:36 PM, "Gabriel Gonzalez" ***@***.***> wrote: @treeowl <https://github.com/treeowl>: Yeah, for the efficient implementation you require the Monad n constraint. In theory you can still do it inefficiently by converting to Control.Monad.Trans.Free.FreeT and then converting back The problem is that adding the Monad n constraint breaks the Control.Monad.Trans.Compose module — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#11 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABzi_TaXl1X99SN6VnAPQQD2LcmJEKVQks5r8PSVgaJpZM4BhqFj> .

[Gabriella439]

You can, using Control.Monad.Trans.Free.Church.{toFT,fromT}, but I just realized it still doesn't work anyway because you still need the Monad n constraint for toFT

[treeowl]

The problem is that adding the Monad n constraint breaks the Control.Monad.Trans.Compose module

While this isn't quite complete, one option is to use constraints:

instance (MFunctor f, MonadTrans f, Lifting Monad g, MonadTrans g) => MonadTrans (ComposeT f g)
  where
    lift :: forall m a. Monad m => m a -> ComposeT f g m a
    lift = ComposeT . hoist lift . lift   \\ (lifting :: Monad m :- Monad (g m))

This requires a Lifting instance for each inner transformer. While that's unfortunate, I'm not convinced that it's more unfortunate than failing to support FT from free. There is even some cause to hope that GHC may eventually be able to provide built-in support for Lifting thanks to recent research on implication constraints.

[Gabriella439]

@treeowl: There's yet another issue, which is that adding a Monad n constraint will break the use case that fixing #29 was designed to solve (i.e. the case where n has kind k -> *). Adding the Monad n constraint would force k to be *, defeating the purpose of making the class poly-kinded

[treeowl]

I don't understand what this polykinded thing has to do with monad morphisms. The `rmap` example seems a bit silly, since `hoist` is already too restrictive to do everything `rmap` can.

…

On Thu, Aug 24, 2017 at 10:34 PM, Gabriel Gonzalez ***@***.*** > wrote: @treeowl <https://github.com/treeowl>: There's yet another issue, which is that adding a Monad n constraint will break the use case that fixing #29 <#29> was designed to solve (i.e. the case where n has kind k -> *). Adding the Monad n constraint would force k to be *, defeating the purpose of making the class poly-kinded — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#11 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABzi_dN5kINPOb87S4jtMUvVMD5K1WYyks5sbjKbgaJpZM4BhqFj> .

[Gabriella439]

Either way, adding the Monad n constraint would be yet another a breaking change due to previously enabling PolyKinds

I also would still like to keep the constraints on the use of hoist as small as possible

[Gabriella439]

Actually, even without considering PolyKinds adding the Monad n constraint is still a breaking change to the API (since there may be some call sites in the wild where n is not a Monad)

[turion]

I just stumbled over the operational example. Even if you implement, as suggested this function:

unviewT :: Monad n => ProgramViewT instr n a -> ProgramT instr n a
unviewT (Return a) = return a
unviewT (instruction :>>= continuation) = singleton instruction >>= continuation

...you still need the Monad n constraint on the target monad. I'd like to use operational and add an MFunctor instance, but unfortunately like this it won't work. Can we reopen and reconsider?

EDIT: I meant operational, not mmorph

[Gabriella439]

@turion: I believe you can implement MFunctor for ProgramT, like this:

instance MFunctor (ProgramT instr m) where
    hoist nat (Lift   m) = Lift (nat m)
    hoist nat (Bind m f) = Bind (hoist nat m) (\x -> hoist nat (f x))
    hoist _   (Instr  i) = Instr i

I have not type-checked that, though

[turion]

You are right indeed! Thank you very much.

[Gabriella439]

You're welcome! 🙂