[Haskell-cafe] A proof that the list monad is not a free monad
David Feuer
david.feuer at gmail.com
Wed Jan 25 14:59:05 UTC 2017
The ConstraintKinds extension just lets you deal with kinds involving
constraints. Turn it on, import the Constraint kind from somewhere (I know
it's exported from GHC.Exts and also from Data.Constraint in the
constraints package; I don't know if it has a nice home in base). Then you
can write things like
class C f a where
p :: f a => proxy f -> a -> Int
etc.
On Jan 23, 2017 4:19 PM, "Olaf Klinke" <olf at aatal-apotheke.de> wrote:
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/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170125/21909ff4/attachment.html>
More information about the Haskell-Cafe
mailing list