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!

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.