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

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/
participants (1)
-
Olaf Klinke