KDS NoTeBook

Free Monad

Free Monad

Initial encoding

by tel on ycombinator:

"Initial" usually means "the initial algebra over a functor". This means that for some functor f the algebra i : f (Initial f) -> Initial f is initial in the category of f algebras. This means that for any X and g : f X -> X there's a universal function universal g : Initial f -> X such that g . fmap (universal g) = universal g . i at type f (Initial f) -> X. Or, we have a function

universal : (f x -> x) -> (Initial f -> x)

and we can actually define Initial in this way

universal' : Initial f -> (f x -> x) -> x

newtype Initial f = Initial { universal' :: forall x . (f x -> x) -> x }

In "strict Haskell" where we can act only finitely, we construct values of Initial f only by slapping finitely many layers of f on top of one another. For instance, when f is data ConsF x = NilF | ConsF Int x we can make a list [1, 2, 3] like

Initial $ \join -> 
  let nil   = join NilF
    a : x = join (ConsF a x)
  in 1 : 2 : 3 : nil

In other words, Initial things are described by their construction.

Clearly, this relates directly to initial objects constructed via, e.g., Free, since it does roughly the same thing. Free emphasizes the notion of layering things atop one another. In Lazy Haskell we can still use this layering to construct non-initial objects (more to come below) but if Free were transported to Strict Haskell it would clearly only construct initial things.

So what about Finally Tagless?

class List l where
  nil :: l
  cons :: Int -> l -> l

We're still going to be constructing values of List l => l by application of finite layers! If anything, we're more stuck to this process now.

cons 1 (cons 2 (cons 3 nil))) :: List l => l

If we swap this out for explicit dictionary passing we can see that we're missing an argument like

data ListD l = ListD { nil :: l, cons :: Int -> l -> l }

\d -> cons d 1 (cons d 2 (cons d 3 nil)) :: ListD l -> l

and also that ListD l is equivalent to ConsF l -> l. It's really the same thing as the free method and is again operating initially.

So what does it take to make something "final"? A final coalgebra of f would be an object i : Final f -> f (Final f) such that for any X and coalgebra g : X -> f X we have universal g : X -> Final f such that i . universal g = fmap (universal g) . g at type X -> f (Final f). Or,

universal : (x -> f x) -> x -> Final f

which again can be used to define Final f

data Final f where
  Final :: (x, x -> f x) -> Final f

No longer can we define things by how they are constructed, now we must define them by how they are viewed. This opens up the doors to new kinds of structures, even in "Strict Haskell"

natsFrom :: Int -> Final ConsF
natsFrom n0 = Final (n0, \n -> ConsF n (natsFrom (n + 1)))

by Adam Warski on SoftwareMill

Что такое Free Monad

StackOverFlow

A Monad is something that "computes" when monadic context is collapsed by join :: m (m a) -> m a (recalling that >>= can be defined as x >>= y = join (fmap y x)). This is how Monads carry context through a sequential chain of computations: because at each point in the series, the context from the previous call is collapsed with the next.

A free monad satisfies all the Monad laws, but does not do any collapsing (i.e., computation). It just builds up a nested series of contexts. The user who creates such a free monadic value is responsible for doing something with those nested contexts, so that the meaning of such a composition can be deferred until after the monadic value has been created.

Free monads are just a general way of turning functors into monads. That is, given any functor f Free f is a monad. This would not be very useful, except you get a pair of functions

liftFree :: Functor f => f a -> Free f a
foldFree :: Functor f => (f r -> r) -> Free f r -> r

the first of these lets you "get into" your monad, and the second one gives you a way to "get out" of it.

More generally, if X is a Y with some extra stuff P, then a "free X" is a a way of getting from a Y to an X without gaining anything extra.

Examples: a monoid (X) is a set (Y) with extra structure (P) that basically says it has an operation (you can think of addition) and some identity (like zero).

So

class Monoid m where
   mempty  :: m
   mappend :: m -> m -> m

Now, we all know lists

data [a] = [] | a : [a]

Well, given any type t we know that [t] is a monoid

instance Monoid [t] where
  mempty   = []
  mappend = (++)

and so lists are the "free monoid" over sets (or in Haskell types).

Okay, so free monads are the same idea. We take a functor, and give back a monad. In fact, since monads can be seen as monoids in the category of endofunctors, the definition of a list

data [a] = [] | a : [a]

looks a lot like the definition of free monads

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

and the Monad instance has a similarity to the Monoid instance for lists

--it needs to be a functor
instance Functor f => Functor (Free f) where
  fmap f (Pure a) = Pure (f a)
  fmap f (Roll x) = Roll (fmap (fmap f) x)

--this is the same thing as (++) basically
concatFree :: Functor f => Free f (Free f a) -> Free f a
concatFree (Pure x) = x
concatFree (Roll y) = Roll (fmap concatFree y)

instance Functor f => Monad (Free f) where
  return = Pure -- just like []
  x >>= f = concatFree (fmap f x)  --this is the standard concatMap definition of bind

now, we get our two operations

-- this is essentially the same as \x -> [x]
liftFree :: Functor f => f a -> Free f a
liftFree x = Roll (fmap Pure x)

-- this is essentially the same as folding a list
foldFree :: Functor f => (f r -> r) -> Free f r -> r
foldFree _ (Pure a) = a
foldFree f (Roll x) = f (fmap (foldFree f) x)

неразобранное

Теория Категорий

Недостатки

неразобранное

Published

Category

programming

Tags