Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Free Monad of a Monad

Is x >>= f equivalent to retract (liftF x >>= liftF . f)?

That is, is the monad instance of a free monad build from a Functor which is also a Monad going to have an equivalent monad instance to the original Monad?

like image 479
singpolyma Avatar asked Feb 06 '13 22:02

singpolyma


People also ask

Why use free monad?

A free monad is a construction which allows you to build a monad from any Functor. Like other monads, it is a pure way to represent and manipulate computations. In particular, free monads provide a practical way to: represent stateful computations as data, and run them.

What is maybe monad?

The Maybe sum type is a versatile and useful data structure that forms a monad. This enables you to compose disparate functions that each may err by failing to return a value.

What is state monad?

The state monad is a built in monad in Haskell that allows for chaining of a state variable (which may be arbitrarily complex) through a series of function calls, to simulate stateful code.

What is a Haskell monad?

A monad is an algebraic structure in category theory, and in Haskell it is used to describe computations as sequences of steps, and to handle side effects such as state and IO. Monads are abstract, and they have many useful concrete instances. Monads provide a way to structure a program.


2 Answers

I don't know what your definition of retract is, but given

retract :: Monad m => Free m a -> m a
retract (Pure a) = return a
retract (Impure fx) = fx >>= retract

and

liftF :: Functor f => f a -> Free f a
liftF fx = Impure (fmap Pure fx)

note that (proofs might be wrong, did them by hand and haven't checked them)

retract $ liftF x
= retract (Impure (fmap Pure x))
= (fmap Pure x) >>= retract
= (x >>= return . Pure) >>= retract
= x >>= \y -> (return $ Pure y) >>= retract
= x >>= \y -> (retract (Pure y))
= x >>= \y -> return y
= x >>= return
= x

so you have

retract (liftF x >>= liftF . f)
= retract ((Impure (fmap Pure x)) >>= liftF . f)
= retract $ Impure $ fmap (>>= liftF . f) $ fmap Pure x
= (fmap (>>= liftF . f) $ fmap Pure x) >>= retract
= (fmap (\y -> Pure y >>= liftF . f) x) >>= retract
= (fmap (liftF . f) x) >>= retract
= (liftM (liftF . f) x) >>= retract
= (x >>= return . liftF . f) >>= retract
= x >>= (\y -> (return $ liftF $ f y >>=  retract)
= x >>= (\y -> retract $ liftF $ f y)
= x >>= (\y -> retract . liftF $ f y)
= x >>= (\y -> f y)
= x >>= f

this does not mean that Free m a is isomorphic to m a, just that retract is really witness to a retraction. Note that liftF is not a monad morphism (return does not go to return). Free is functor in the category of functors, but it is not a monad in the category of monads (despite retract looking a lot like join and liftF looking a lot like return).

EDIT: Note that the retraction implies a sort of equivalence. Define

 ~ : Free m a -> Free m a -> Prop
 a ~ b = (retract a) ==_(m a) (retract b)

Then consider the quotient type Free m a/~. I assert that this type is isomorphic to m a. Since (liftF (retract x)) ~ x because (retract . liftF . retract $ x) ==_(m a) retract x. Thus, the free monad over a monad is exactly that monad plus some extra data. This is exactly the same as the claim that [m] is "essentially the same" as m when m is m is a monoid.

like image 110
Philip JF Avatar answered Sep 21 '22 14:09

Philip JF


That is, is the monad instance of a free monad build from a Functor which is also a Monad going to have an equivalent monad instance to the original Monad?

No. The free monad over any functor is a monad. Thus, it cannot magically know about the Monad instance when it exists. And it cannot also "guess" it, because the same functor may be made a Monad in different ways (e.g. a writer monad for different monoids).

Another reason is that it doesn't make much sense to ask whether these two monads have equivalent instances because they are not even isomorphic as types. For example, consider the free monad over the writer monad. It will be a list-like structure. What does it mean for these two instances to be equivalent?

Example of different monad instances

In case the above description isn't clear, here's an example of a type with many possible Monad instances.

data M a = M Integer a

bindUsing :: (Integer -> Integer -> Integer) -> M a -> (a -> M b) -> M b
bindUsing f (M n a) k =
  let M m b = k a
  in M (f m n) b

-- Any of the below instances is a valid Monad instance
instance Monad M where
  return x = M 0 x
  (>>=) = bindUsing (+)

instance Monad M where
  return x = M 1 x
  (>>=) = bindUsing (*)
like image 30
Roman Cheplyaka Avatar answered Sep 20 '22 14:09

Roman Cheplyaka