Difference between free monads and fixpoints of functors?

36
votes

I was reading http://www.haskellforall.com/2013/06/from-zero-to-cooperative-threads-in-33.html where an abstract syntax tree is derived as the free monad of a functor representing a set of instructions. I noticed that the free monad Free is not much different from the fixpoint operator on functors Fix.

The article uses the monad operations and do syntax to build those ASTs (fixpoints) in a concise way. I'm wondering if that's the only benefit from the free monad instance? Are there any other interesting applications that it enables?

2
haskellcategory-theoryfree-monadfixpoint-combinators
The main benefit of the monad instance is do notation and reuse of combinators from Control.Monad (like replicateM_ and forM_ in the examples). A common trick is to build up the type using a free monad but then demand that the result has type FreeT f m Void so that it can be converted to the fixed point of a functor. – Gabriella Gonzalez
The Monad instance enriches Fix with two things--definite termination from return and natural "extension" from (>>=). A regular (Fix f) cannot be guaranteed to have any (finite) values at all (i.e. (Fix Identity)), but (Free f) is always inhabited at least by Pure. – J. Abrahamson
@DanielVelkov You use the Void return trick whenever you want to get the best of both worlds: i.e. use a free monad to assemble the data type and then use an F-algebra to interpret it. The Void return value enforces that the free monad you build is isomorphic to the fixed point of the base functor when you are done. – Gabriella Gonzalez
The main advantage of porting morphisms from Fix to Free is if you want to use do notation or combinators from Control.Monad. If you don't need those things and you can assemble Fix values by hand then there is no need to go through the Free intermediate. Just think of FreeT f m Void as a convenient monadic way way to build up values of type Fix that is a bit more beginner friendly. – Gabriella Gonzalez
Fix has the advantage of being a newtype which might make it easier for the compiler to rip off layers, but I'm not sure in light of all the final/CPS encodings of free that are lying about. – J. Abrahamson

2 Answers

18
votes

(N.B. this combines a bit from both mine and @Gabriel's comments above.)

It's possible for every inhabitant of the Fixed point of a Functor to be infinite, i.e. let x = (Fix (Id x)) in x === (Fix (Id (Fix (Id ...)))) is the only inhabitant of Fix Identity. Free differs immediately from Fix in that it ensures there is at least one finite inhabitant of Free f. In fact, if Fix f has any infinite inhabitants then Free f has infinitely many finite inhabitants.

Another immediate side-effect of this unboundedness is that Functor f => Fix f isn't a Functor anymore. We'd need to implement fmap :: Functor f => (a -> b) -> (f a -> f b), but Fix has "filled all the holes" in f a that used to contain the a, so we no longer have any as to apply our fmap'd function to.

This is important for creating Monads because we'd like to implement return :: a -> Free f a and have, say, this law hold fmap f . return = return . f, but it doesn't even make sense in a Functor f => Fix f.

So how does Free "fix" these Fixed point foibles? It "augments" our base functor with the Pure constructor. Thus, for all Functor f, Pure :: a -> Free f a. This is our guaranteed-to-be-finite inhabitant of the type. It also immediately gives us a well-behaved definition of return.

return = Pure

So you might think of this addition as taking out potentially infinite "tree" of nested Functors created by Fix and mixing in some number of "living" buds, represented by Pure. We create new buds using return which might be interpreted as a promise to "return" to that bud later and add more computation. In fact, that's exactly what flip (>>=) :: (a -> Free f b) -> (Free f a -> Free f b) does. Given a "continuation" function f :: a -> Free f b which can be applied to types a, we recurse down our tree returning to each Pure a and replacing it with the continuation computed as f a. This lets us "grow" our tree.

Now, Free is clearly more general than Fix. To drive this home, it's possible to see any type Functor f => Fix f as a subtype of the corresponding Free f a! Simply choose a ~ Void where we have data Void = Void Void (i.e., a type that cannot be constructed, is the empty type, has no instances).

To make it more clear, we can break our Fix'd Functors with break :: Fix f -> Free f a and then try to invert it with affix :: Free f Void -> Fix f. 

break (Fix f) = Free (fmap break f) 
affix (Free f) = Fix (fmap affix f)

Note first that affix does not need to handle the Pure x case because in this case x :: Void and thus cannot really be there, so Pure x is absurd and we'll just ignore it.

Also note that break's return type is a little subtle since the a type only appears in the return type, Free f a, such that it's completely inaccessible to any user of break. "Completely inaccessible" and "cannot be instantiated" give us the first hint that, despite the types, affix and break are inverses, but we can just prove it.

(break . affix) (Free f)
===                                     [definition of affix]
break (Fix (fmap affix f))
===                                     [definition of break]
Free (fmap break (fmap affix f))
===                                     [definition of (.)]
Free ( (fmap break . fmap affix) f )
===                                     [functor coherence laws]
Free (fmap (break . affix) f)

which should show (co-inductively, or just intuitively, perhaps) that (break . affix) is an identity. The other direction goes through in a completely identical fashion.

So, hopefully this shows that Free f is larger than Fix f for all Functor f.

So why ever use Fix? Well, sometimes you only want the properties of Free f Void due to some side effect of layering fs. In this case, calling it Fix f makes it more clear that we shouldn't try to (>>=) or fmap over the type. Furthermore, since Fix is just a newtype it might be easier for the compiler to "compile away" layers of Fix since it only plays a semantic role anyway.

  • Note: we can more formally talk about how Void and forall a. a are isomorphic types in order to see more clearly how the types of affix and break are harmonious. For instance, we have absurd :: Void -> a as absurd (Void v) = absurd v and unabsurd :: (forall a. a) -> Void as unabsurd a = a. But these get a little silly.
10
votes

There is a deep and 'simple' connection.

It's a consequence of adjoint functor theorem, left adjoints preserve initial objects: L 0 ≅ 0.

Categorically, Free f is a functor from a category to its F-algebras (Free f is left adjoint to a forgetful functor going the other way 'round). Working in Hask our initial algebra is Void

Free f Void ≅ 0

and the initial algebra in the category of F-algebras is Fix f: Free f Void ≅ Fix f

import Data.Void
import Control.Monad.Free

free2fix :: Functor f => Free f Void -> Fix f
free2fix (Pure void) = absurd void
free2fix (Free body) = Fix (free2fix <$> body)

fixToFree :: Functor f => Fix f -> Free f Void
fixToFree (Fix body) = Free (fixToFree <$> body)

Similarly, right adjoints (Cofree f, a functor from Hask to the category of F-coalgebras) preserves final objects: R 1 ≅ 1.

In Hask this is unit: () and the final object of F-coalgebras is also Fix f (they coincide in Hask) so we get: Cofree f () ≅ Fix f

import Control.Comonad.Cofree

cofree2fix :: Functor f => Cofree f () -> Fix f
cofree2fix (() :< body) = Fix (cofree2fix <$> body)

fixToCofree :: Functor f => Fix f -> Cofree f ()
fixToCofree (Fix body) = () :< (fixToCofree <$> body)

Just look how similar the definitions are!

newtype Fix f 
  = Fix (f (Fix f))

Fix f is Free f with no variables.

data Free f a 
  = Pure a 
  | Free (f (Free f a))

Fix f is Cofree f with dummy values.

data Cofree f a 
  = a <: f (Cofree f a)