Add a MonadBaseControl instance for CofreeT

treeowl commented 4 years ago

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 https://github.com/basvandijk/monad-control/issues/48.

treeowl commented 4 years ago

`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 commented 4 years ago

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 commented 3 years ago

@RyanGlScott, what do you think?

RyanGlScott commented 3 years ago

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 commented 3 years ago

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 notifications@github.com 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 https://github.com/ekmett/free/issues/193#issuecomment-752054540, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAOOF7KT4LA34KMGZRXT2RDSXHBV3ANCNFSM4I2Q7YOA .

fumieval commented 3 years ago

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.

ekmett / free