Does MonadFree have enough firepower?

[redxaxder]

The statement that the monad m is free over the functor f corresponds to the following universal property:

Given a monad m' and a natural transformation n: f ~> m' there exists a unique monad morphism nhat: m ~> m' such that nhat . wrap . fmap return == n.

So it should be possible to write the following generalization of foldFree:

phi :: (MonadFree f m, Monad m') => (forall x. f x -> m' x) -> m a -> m' a

but it appears to me that wrap :: f (m a) -> m a is not sufficient for this. I find myself itching for something like unwrap :: m a -> Either a (f m a).

[ElvishJerricco]

These properties can't be represented with the free Monad transformer.

On Thu, Feb 2, 2017 at 11:07 PM redxaxder [email protected] wrote:

The statement that the monad m is free over the functor f corresponds to the following universal property:

Given a monad m' and a natural transformation n: f ~> m' there exists a unique monad morphism nhat: m ~> m' such that nhat . wrap . fmap return == n.

So it should be possible to write the following generalization of foldFree:

phi :: (MonadFree f m, Monad m') => (forall x. f x -> m' x) -> m a -> m' a

but it appears to me that wrap :: f (m a) -> m a is not sufficient for this. I find myself itching for something like unwrap :: m a -> Either a (f m a).

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ekmett/free/issues/147, or mute the thread https://github.com/notifications/unsubscribe-auth/ABTWvLvCrvH3vCpRr8zSHOAg5_t2uxozks5rYqgLgaJpZM4L18PQ .

[redxaxder]

So the proper interpretation of an instance of MonadFree f m isn't as a statement that "the monad m is free over f" but rather as an mtl-style constraint.

[ElvishJerricco]

I guess that depends on whether FreeT f m is "free over f".

[redxaxder]

I don't think so. If it was then it would be possible to write the function phi :: (Monad m, Monad m') => (forall x. f x -> m' x) -> FreeT f m a -> m' a, but m' can be Identity so this would require a backdoor that can escape an arbitrary monad.

[ElvishJerricco]

Right, it's not with that definitions. Was just wondering if there's a suitable definition for "free over f" that satisfies both FreeT and the categorical semantics. Can't think of anything though.

[masaeedu]

If I understand correctly, in order to align with the category theoretic definition of free, you need a functor from the category of functors to the category of monads, i.e. a type constructor T :: (* -> *) -> (* -> *), and an instance of the class:

class (forall f. Functor f => Monad (t f)) => FMFunctor t where
  fmmap :: (Functor a, Functor b) => (a :~> b) -> (t a :~> t b)

Then, provided additionally that there is an implementation of:

class FMFunctor t => FreeFMFunctor t where
  up     :: a :~> t a
  across :: (Functor i, Monad o) => (i :~> o) -> (t i :~> o)

, we can say that T is one of many isomorphic free functors from the category of functors to the category of monads.

Free has instances for both of these classes.

When talking about FreeT, we have to recognize that it's actually the free functor from the category of endofunctors on Hask not to the category of monads, but rather to the category of monad transformers (or equivalently the category of pointed endofunctors on the category of monads on Hask). Here's all the busywork to describe the classes for that, and witness the FreeT instances:

{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE TypeInType            #-}

import Control.Monad.Trans.Class
import Control.Monad.Trans.Free
import Control.Monad.Identity

type a :>   b = forall x.            a   ->  b
type a :~>  b = forall x.            a x :>  b x
type a :~~> b = forall x. Monad x => a x :~> b x

-- F: the category of endofunctors on Hask
-- FM: the category of endofunctors on the category of monads on Hask

-- A functor from F to FM
class (forall f. Functor f => MonadTrans (t f)) => FMFFunctor t where
  fmfmap :: (Functor a, Functor b) => (a :~> b) -> (t a :~~> t b)

-- FreeT is such a functor
instance FMFFunctor FreeT where
  fmfmap = transFreeT

-- Need this so that the instance for the output monad is in scope
class (MonadTrans t, forall m. Monad m => Monad (t m)) => MonadTrans' t
instance Functor f => MonadTrans' (FreeT f)

-- The forgetful functor FM to F
type FMFForget h a = forall m. Monad m => h m a

-- The *free* functor from F to FM
class FMFFunctor t => FreeFMFFunctor t where
  up     :: Functor i     => i :~> FMFForget (t i)
  across :: MonadTrans' o => (i :~> FMFForget o) -> (t i :~~> o)

-- FreeT is also that functor
instance FreeFMFFunctor FreeT where
  up = liftF
  across = foldFreeT