Mon Jan 23 21:17:07 UTC 2017

```On a mostly unrelated note, Dan Doel elaborated  that the list monad is not the monad of free monoids either, even though mathematically the free monoid over x is the set of words of finite length with alphabet x. Briefly, the reason is that Haskell types are domains, not sets.

Below is a proof that the free monad is not the free algebra.

One approximant to free algebraic structures is to look at the free F-algebra for a functor F. This approach does not take into account any equations between the algebraic operations.

{-# LANGUAGE Rank2Types,MultiParamTypeClasses,FlexibleInstances,FlexibleContexts #-}
module FreeFAlg where
import Control.Applicative

-- F-algebras (sans laws).
class Functor f => Alg f a where
alg :: f a -> a

-- The free F-algebra over x, following Dan Doel's ideas,
-- with the universal property baked in.
newtype FreeAlg f x = FreeAlg (forall a. Alg f a => (x -> a) -> a)
runFree :: Alg f a => FreeAlg f x -> (x -> a) -> a
runFree (FreeAlg f) = f
universal :: Alg f a => (x -> a) -> FreeAlg f x -> a
universal = flip runFree
instance Functor f => Alg f (FreeAlg f x) where
alg ff = FreeAlg (\f -> alg (fmap ((\$f).runFree) ff))
instance Functor (FreeAlg f) where
fmap h (FreeAlg fx) = FreeAlg (\f -> fx (f.h))
return x = FreeAlg (\$x)
(FreeAlg fx) >>= k = FreeAlg (\f -> fx (\x -> runFree (k x) f))
instance Applicative (FreeAlg f) where
pure = return
(<*>) = ap

data FreeMonad f x = Pure x | Roll (f (FreeMonad f x))
instance Functor f => Alg f (FreeMonad f x) where
alg = Roll

-- This looks like the same universal property...
universal' :: Alg f a => (x -> a) -> FreeMonad f x -> a
universal' f (Pure x) = f x
universal' f (Roll ffree) = alg  (fmap (universal' f) ffree)

freeAlg2freeMonad :: Functor f => FreeAlg f x -> FreeMonad f x
freeMonad2freeAlg :: Functor f => FreeMonad f x -> FreeAlg f x

The free monad is not the free F-algebra, because uniqueness fails.
Consider the constant functor

data Point a = Point
instance Functor Point where
fmap f Point = Point
-- universal' f (Pure x) = f x
-- universal' f (Roll Point) = alg Point
-- but we have another function with the same type as universal':
notUnique :: Alg Point a => (x -> a) -> FreeMonad Point x -> a
notUnique f = const (alg Point)

For classes like Monoid, which have equations between the algebraic operations (such as mappend mempty = id), we'd need the language extension that allows constraints as type parameters. I'd like to write

Free Monoid x = Free (forall a. Monid a => (x -> a) -> a)

but I am not experienced with the ConstraintKinds extension. Anyone help?

Olaf