[Haskell-cafe] A proof that the list monad is not a free monad
Olaf Klinke
olf at aatal-apotheke.de
Mon Jan 23 21:17:07 UTC 2017
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/
More information about the Haskell-Cafe
mailing list