Add a MonadBaseControl instance for CofreeT

[treeowl]

The following certainly typechecks:

instance (Alternative f, MonadBaseControl b m)
         => MonadBaseControl b (CofreeT f m) where
  type StM (CofreeT f m) a = StM m (CofreeF f a (CofreeT f m a))
  liftBaseWith f = CofreeT $ liftBaseWith $
                              \g -> (:< empty) <$> f (g . runCofreeT)
  restoreM q = CofreeT $ restoreM q

I believe it obeys the MonadTransControl laws under the assumption using the fact that

forall f q.  f <$> liftBaseWith q = liftBaseWith $ \rib -> fmap f (q rib)

While this strikes me as reasonable, I don't have enough experience with the class to know for sure. See basvandijk/monad-control#48.

[treeowl]

liftBaseWith laws

liftBaseWith $ const $ return x
= CofreeT $ liftBaseWith $ \g -> (:< empty) <$> const (return x) (g . runCofreeT)
= CofreeT $ liftBaseWith $ \g -> (:< empty) <$> return x
= CofreeT $ liftBaseWith $ \g -> return (x :< empty)
= CofreeT $ liftBaseWith $ const $ return (x :< empty)
= CofreeT $ return (x :< empty)
= return x

This one can surely be compressed some:

liftBaseWith (const (m >>= f))
= CofreeT $ liftBaseWith $ \g -> (:< empty) <$> const (m >>= f) (...)
= CofreeT $ liftBaseWith $ const $ (:< empty) <$> m >>= f
= CofreeT $ liftBaseWith $ const $ m >>= \x -> f x >>= pure . (:< empty)
= CofreeT $ liftBaseWith $ const ((m >>= f) >>= pure . (:< empty))
= CofreeT $ liftBaseWith (const (m >>= f)) >>= liftBaseWith . const . pure . (:< empty)
= CofreeT $ liftBaseWith (const (m >>= f)) >>= pure . (:< empty)
= CofreeT $ (liftBaseWith (const m) >>= liftBaseWith . const . f) >>= pure . (:< empty)

= CofreeT $ liftBaseWith (const m) >>=
                          \a -> (liftBaseWith . const . f) a >>=
                                      \b -> pure (b :< empty)

= CofreeT $ do
    a <- liftBaseWith (const m)
    b <- liftBaseWith (const (f a))
    return $ b :< empty

= CofreeT $ do
    a <- liftBaseWith (const m)
    b <- liftBaseWith (const (f a))
    return $ b :< (empty <|> fmap (>>= liftBaseWith . const . f) empty)

= CofreeT $ do
    a :< m' <- (:< empty) <$> liftBaseWith (const m)
    b :< n <- (:< empty) <$> liftBaseWith (const (f a))
    return $ b :< (n <|> fmap (>>= liftBaseWith . const . f) m')

= CofreeT $ do
    a :< m' <- liftBaseWith (const m) >>= pure . (:< empty)
    b :< n <- liftBaseWith (const (f a)) >>= pure . (:< empty)
    return $ b :< (n <|> fmap (>>= liftBaseWith . const . f) m')

= CofreeT $ do
    a :< m' <- liftBaseWith (const m) >>= liftBaseWith . const . pure . (:< empty)
    b :< n <- liftBaseWith (const (f a)) >>= liftBaseWith . const . pure . (:< empty)
    return $ b :< (n <|> fmap (>>= liftBaseWith . const . f) m')

= CofreeT $ do
    a :< m' <- liftBaseWith $ const $ m >>= pure . (:< empty)
    b :< n <- liftBaseWith $ const $ f a >>= pure . (:< empty)
    return $ b :< (n <|> fmap (>>= liftBaseWith . const . f) m')

= CofreeT $ do
    a :< m' <- liftBaseWith $ \_ -> (:< empty) <$> m
    b :< n <- liftBaseWith $ \_ -> (:< empty) <$> f a
    return $ b :< (n <|> fmap (>>= liftBaseWith . const . f) m')

= (CofreeT $ liftBaseWith $ \_ -> (:< empty) <$> m)
    >>= \x -> CofreeT $ liftBaseWith $ \_ -> (:< empty) <$> f x
= liftBaseWith (const m) >>= \x -> liftBaseWith $ const (f x)

restoreM law

liftBaseWith (\runInBase -> runInBase m) >>= restoreM
= (CofreeT $ liftBaseWith $ \g -> (:< empty) <$> g (runCofreeT m))
     >>= CofreeT . restoreM
= CofreeT $ do
    a :< m' <- liftBaseWith $ \g -> (:< empty) <$> g (runCofreeT m)
    b :< n <- restoreM a
    return $ b :< (n <|> fmap (>>= CofreeT . restoreM) m')

-- Invoking my assumption

= CofreeT $ do
    a :< m' <- (:< empty) <$> liftBaseWith $ \rib -> rib $ runCofreeT m
    b :< n <- restoreM a
    return $ b :< (n <|> fmap (>>= CofreeT . restoreM) m')
= CofreeT $ do
    a <- liftBaseWith $ \rib -> rib $ runCofreeT m
    b :< n <- restoreM a
    return $ b :< n
= CofreeT $ do
    b :< n <- runCofreeT m
    return $ b :< n
= m

[treeowl]

The extra law is a free theorem, as Li-Yao Xia explains. So we can do this if it makes some kind of sense.

[treeowl]

@RyanGlScott, what do you think?

[RyanGlScott]

To be honest, I haven't really used monad-control much, so I don't have a strong opinion on it. Since @ekmett has expressed reservations about adding instances from monad-control in the past (see here), I'd like to hear his opinion before going forth and adding a monad-control dependency.

[treeowl]

I'm more asking your opinion about whether it makes sense than whether it should be added here.

…

On Tue, Dec 29, 2020, 7:13 AM Ryan Scott ***@***.***> wrote: To be honest, I haven't really used monad-control much, so I don't have a strong opinion on it. Since @ekmett <https://github.com/ekmett> has expressed reservations about adding instances from monad-control in the past (see here <#m_3502922702521140048_20>), I'd like to hear his opinion before going forth and adding a monad-control dependency. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#193 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOOF7KT4LA34KMGZRXT2RDSXHBV3ANCNFSM4I2Q7YOA> .

[fumieval]

I personally think we should avoid MonadBaseControl as much as possible. It makes forking and exception handling of stateful monad transformers "work", but often in undesirable ways. Maybe it makes sense if monad-control didn't have the footgun instances for StateT, ExceptT and so on, but it does so it's hard to say for me that the proposed instance makes sense.