A proof that the list monad is not a free monad

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

A proof that the list monad is not a free monad

Ingo Blechschmidt
Dear lovers of generalized abstract nonsense,

recall that we can construct, for any functor f, the free monad over f:

    data Free f a = Pure a | Roll (f (Free f a))

Intuitively, Free f a is the type of f-shaped trees with leaves of type a.
The join operation merely grafts trees together and doesn't perform any
further computations. Values of the form (Roll _) shall be called
"nontrivial" in this posting.

Some of the usual monads are in fact free monads over some functor:

* The Tree monad is the free monad over the functor Pair, where
  data Pair a = MkPair a a. The intuition as Pair-shaped trees
  is most strong in this example. Every parent node has a pair of
  children.

* The Maybe monad is the free monad over the functor Unit, where
  data Unit a = MkUnit. In the graphical picture parent nodes have a
  Unit of children, so no children at all. So there are exactly two
  Unit-shaped trees: the tree consisting only of a leaf (corresponding
  to Just _) and the three consisting of a childless parent node
  (corresponding to Nothing).

* The Identity monad is the free monad over the functor Void,
  where Void a is a type without constructors.

* The Partiality monad is the free monad over Maybe.

* The Writer [r] monad is the free monad over the functor (r,).
  In an (r,)-shaped tree, a parent node is decorated with a value
  of type r and has exactly one child node. Traversing such a path
  yields a list of r's and a leaf value of type a, so in total
  a value of type ([r],a) = Writer r a.

  (In particular, Free (r,) () is isomorphic to [r]. This observation
  led to the claim that the list monad is free. But this claim is false
  and indeed doesn't follow from the observation. To show that a monad m
  is free, one has to exhibit a monad isomorphism forall a. m a -> Free f a
  for some functor f. In contrast, exhibiting an isomorphism of m a with
  Free (f a) () is neither sufficient nor required.)

Even more monads are quotients of free monads. For instance, State s is
a quotient of Free (StateF s), where

    data StateF s a = Put s a | Get (s -> a).
    -- NB: This functor is itself a free functor over a type constructor
    -- which is sometimes called StateI [1], rendering Free (StateF s) what
    -- Oleg and Hiromi Ishii call a "freer monad" [2].

The quotient is exhibited by the following monad morphism, which gives
semantics to the purely syntactical values of the free monad.

    run :: Free (StateF s) a -> State s a
    run (Pure x)         = return x
    run (Roll (Put s m)) = put s >> run m
    run (Roll (Get k))   = get >>= run . k

This point of view is the basis of the operational package by apfelmus [1]
and is also talked about in an StackOverflow thread [3]. It's the main
reason why free monads are useful in a programming context.

So, is the list monad a free monad? Intuitively, it's not, because the
join operation of the list monad (concatenation) doesn't merely graft
expressions together, but flattens them [4].

Here is a proof that the list monad is not free. I'm recording it since
I've been interested in a proof for quite some time, but searching for
it didn't yield any results. The threads [3] and [5] came close, though.

In the free monad over any functor, the result of binding a nontrivial
action with any function is always nontrivial, i.e.

    (Roll _ >>= _) = Roll _

This can be checked directly from the definition of (>>=) for the free
monad or alternatively with Reid Barton's trick of exploiting a monad
morphism to Maybe, see [3].

If the list monad was isomorphic-as-a-monad to the free monad over some
functor, the isomorphism would map only singleton lists [x] to values of
the form (Pure _) and all other lists to nontrivial values. This is
because monad isomorphisms have to commute with "return" and return x
is [x] in the list monad and Pure x in the free monad.

These two facts contradict each other, as can be seen with the following
example:

    do
        b <- [False,True]  -- not of the form (return _)
        if b
            then return 47
            else []
    -- The result is the singleton list [47], so of the form (return _).

After applying a hypothetical isomorphism to the free monad over some
functor, we'd have that the binding of a nontrivial value (the image
of [False,True] under the isomorphism) with some function results in a
trivial value (the image of [47], i.e. return 47).

Cheers,
Ingo

[1] http://projects.haskell.org/operational/Documentation.html
[2] http://okmij.org/ftp/Haskell/extensible/more.pdf
[3] http://stackoverflow.com/questions/14641864/what-monads-can-be-expressed-as-free-over-some-functor
[4] https://hackage.haskell.org/package/free-4.12.4/docs/Control-Monad-Free.html
[5] https://www.reddit.com/r/haskell/comments/50zvyb/why_is_liststate_not_a_free_monad/
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: 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/
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: 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" <[hidden email]> 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.


_______________________________________________
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.