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. |
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. |
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. _______________________________________________ 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. |
Free forum by Nabble | Edit this page |