Did this construction of free(freer?) monad works?

Question

In the past 2 years, I was interested in using free monad to helping me to solve practical software engineering problem. And came up my own construction of free monad using some elementary category theory.

{-# LANGUAGE RankNTypes #-}

import Control.Monad

data Free f a = Free (forall m. Monad m => (forall x. f x -> m x) -> m a)

runFree :: forall f m. Monad m => (forall x. f x -> m x) -> (forall a. Free f a -> m a)
runFree f (Free g) = g f

instance Functor (Free f) where
  fmap f (Free g) = Free $ \k -> fmap f (g k)

instance Applicative (Free f) where
  pure = return
  (<*>) = ap

instance Monad (Free f) where
  return a = Free $ \_ -> return a
  Free f >>= g = Free $ \k -> f k >>= \a -> runFree k (g a)

liftF :: forall f a. f a -> Free f a
liftF x = Free $ \k -> k x

Intuitively. Free just passing an interpreter around the context. The interpreter just transform a functor(or a type constructor) to the actual monad. In category theory, this is just a natural transformation between functors. runFree function just unravel it and apply the interpreter.

In short, at the theoretical level. Consider the following adjoint functor: (Free : Endo -> Monad) ⊣ (Forgetful : Monad -> Endo).We have the following adjunction isomorphism: Monad(Free f, m) ~ Endo(f, Forgetful m). Which translate to haskell are the following function:

alpha :: forall f m. Monad m => (forall a. Free f a -> m a) -> (forall x. f x -> m x)
beta  :: forall f m. Monad m => (forall x. f x -> m x) -> (forall a. Free f a -> m a)

Then we can construct Free based on beta:

data Free f a = Free (forall m. Monad m => (forall x. f x -> m x) -> m a)

Which just wraps it in a data type. And the rest just follow.

So I'm just wondering how good(or bad) is this construction of free monad. It seems to me to have the benefit of freer monad: not need to deal with functor instance. Looks intuitive, straight and clean. It also seems to me have no performance problem that freer monad originally need to deal with. So no more complication needed. In total, looks pretty decent for me.

And also because I came up of it myself. I'm wondering did someone already using this construction of free monad? And what's your opinion about it? Thanks!

Edit:

About my own usage about this construction of free monad in programming. I'm mostly using free monad to express monadic DSLs. And later I can interpret them in multiple ways whatever I want. Like I want to build a command handling system defined by monadic DSL. And also want to extract it's meta information to tree like structure(reflection on DSL itself). So I can build two interpreter to do the job. One for executing command and another for transform DSL to tree like structure. Or maybe I want to run the same DSL in different runtime environment. Then I can write appropriate interpreter for each of them without introducing boilerplate code. I found out those use cases are in general very easy and suitable for free monad to deal with. Hope my experience will be useful to you!

Useful

I would use newtype instead of data here. Also, it would be more conventional to write runFree :: forall f m a. Monad m => (forall x. f x -> m x) -> Free f a -> m a. – Blake

Reminds me of the monoid impredicative encoding for lists List A = forall M. Monoid M => (a -> M) -> M. Could be useful for iterating over monads in a similar way to how Foldable is used – Nuggar

I'm not a category theorist, but I believe this is correct. It's very similar to Control.Applicative.Free.Final. – Blake

@Blake Yes. newtype is surely better here. I just wrote example code a few hours ago. So didn't bother about optimizations. And indeed Control.Applicative.Free.Final looks pretty similar. I'm wondering what's the implications about the connections between these... – Useful

@MolossusSpondee Yes. Got the ideas to trying this construction from monoid. Because in general, Monad is just the monoid in the category of endofunctors. : ) – Useful

Answer 1

Yes, your encoding is correct. The free monad Free F over an endofunctor F is also the initial object of the category F-Mon whose

• objects are monads M equipped with "algebras" a :: forall x. F x -> M x (which are equivalently algebraic operations on M, ie, natural transformations a' :: forall x. F (M x) -> M x satisfying a' . fmap join = join . a' ), and
• arrows are natural transformations that are both monad homomorphisms and algebra homomorphisms.

Loosely speaking, your encoding forall m. Monad m => (forall x. F x -> m x) -> m a exactly denotes the initial object in the category F-Mon, just like forall x. x denotes the initial object in the base category, and forall m. Monad m => m a denotes the initial monad (the identity monad).

For programming purposes, this encoding behaves similarly to the Church encoding of free monads forall x. (f x -> x) -> (a -> x) -> x (or the codensity transformation of the conventional free monads): they support O(1) time monadic binding, but no longer support O(1) pattern matching (thus they are not suitable for shallow handlers of computational effects).

I don't remember papers discussing exactly this encoding, but it is probably folklore among people working on computational effects or algebraic theories. For example, in the Haskell community, Wu and Schrijvers [2014] used the category I mentioned earlier for the purpose of fusing handlers; and in the study of algebraic theories, Fiore and Hur [2009] discussed the more general notion of Σ-monoids.

Pani

Yes. This is roughly what i'm thinking before. Thanks for your answer! – Useful

The bit that confuses me is that this construction is a bit different than the traditional encoding data Free f a = Pure a | Free (f (Free f a)), the latter requiring a Functor f instance. So it seems these "free" constructions must relate to different "forgetful" functors? Does this just turn out not to matter in Haskell because fmap is always unique? – Blake

Great observation! Indeed we can take the OP's Free as a functor from |*| -> * to the category of monads where the |*| is the discrete category of *. And yes, even if we first forget a functor <F, fmap> as merely F :: |*| -> *, OP's construction Free F still results in a monad isomorphic to the traditional free monad construction on <F, fmap>. This possibly surprising fact is indeed because of the reason you mentioned, every two functors instances <F, fmap1> and <F, fmap2> in Haskell are isomorphic due to parametricity. – Pani

This thing can be possibly better understood if we rigorously work in the setting of free monads of finitary functors on the category of sets (or any locally finitely presentable category), rather than informally working in the so-called "category" Hask (which I referred to as *). In this setting, a finitary functor is indeed determined by its object mapping on finite sets, so forgetting its arrow mapping is unproblematic (and can be recovered by a left Kan extension). – Pani

Sorry, your explanation went way over my non-existent knowledge of category theory, but I'm glad what I said apparently made some kind of sense! – Blake

This encoding of free monad can be understood in a simpler analogy: free monoid on a type t can be defined as fm t = forall a. Monoid a => (t -> a) -> a. Note that, without any typeclass constraint, the type forall a. (t -> a) -> a is equivalent to just t. But if we require that a is a lawful Monoid then fm t is also a lawful Monoid for all t. By analogy, your encoding of "free monad" is correct and satisfies all required laws. – Thomson