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

[David Feuer]

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>