[Haskell-cafe] A proof that the list monad is not a free monad

[Olaf Klinke]

On a mostly unrelated note, Dan Doel elaborated [1] 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
import Control.Monad

-- 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))
instance Monad (FreeAlg f) where
    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 
freeAlg2freeMonad = universal Pure
freeMonad2freeAlg :: Functor f => FreeMonad f x -> FreeAlg f x
freeMonad2freeAlg = universal' return

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

[1] http://comonad.com/reader/2015/free-monoids-in-haskell/