Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Is there a generalization of these Free-like constructions?

I was playing around with free-like ideas, and found this:

{-# LANGUAGE RankNTypes #-}

data Monoid m = Monoid { mempty :: m, mappend :: m -> m -> m }
data Generator a m = Generator { monoid :: Monoid m, singleton :: a -> m }

newtype Free f = Free { getFree :: forall s. f s -> s }

mkMonoid :: (forall s. f s -> Monoid s) -> Monoid (Free f)
mkMonoid f = Monoid {
    mempty = Free (mempty . f),
    mappend = \a b -> Free $ \s -> mappend (f s) (getFree a s) (getFree b s)
}

freeMonoid :: Monoid (Free Monoid)
freeMonoid = mkMonoid id

mkGenerator :: (forall s. f s -> Generator a s) -> Generator a (Free f)
mkGenerator f = Generator {
    monoid = mkMonoid (monoid . f),
    singleton = \x -> Free $ \s -> singleton (f s) x
}

freeGenerator :: Generator a (Free (Generator a))
freeGenerator = mkGenerator id

I would like to find the conditions under which I could write a funcion:

mkFree :: (??? f) => f (Free f)

but I have been unable to find a meaningful structure for f (other than the trivial one in which mkFree is a method of ???) which would allow this function to be written. In particular, my aesthetic sense would prefer if this structure did not mention the Free type.

Has anyone seen something like this before? Is this generalization possible? Is there a known generalization in a direction that I have not thought of yet?

like image 219
luqui Avatar asked Feb 13 '13 11:02

luqui


1 Answers

The link to universal algebra was a good starting point, and after reading up on it a bit everything fell into place. What we're looking for is an F-algebra:

type Alg f x = f x -> x

for any (endo)functor f. For example, for a Monoid algebra the functor is:

data MonoidF m = MEmpty | MAppend m m deriving Functor

For any Monoid instance there's the obvious monoid algebra:

monoidAlg :: Monoid m => Alg MonoidF m
monoidAlg MEmpty = mempty
monoidAlg (MAppend a b) = mappend a b

Now we can take the free functor definition from the free-functors package, and replace the class constraint with the f-algebra:

newtype Free f a = Free { runFree :: forall b. Alg f b -> (a -> b) -> b }

The free functor is in some sense the best way to turn any set a into an algebra. This is how:

unit :: a -> Free f a
unit a = Free $ \_ k -> k a

It is the best way because for any other way to turn a into an algebra b, we can give a function from the free algebra to b:

rightAdjunct :: Functor f => Alg f b -> (a -> b) -> Free f a -> b
rightAdjunct alg k (Free f) = f alg k

What is left is to actually show that the free functor creates an f-algebra (and this is what you asked for):

freeAlg :: Functor f => Alg f (Free f a)
freeAlg ff = Free $ \alg k -> alg (fmap (rightAdjunct alg k) ff)

To explain a bit: ff is of type f (Free f a) and we need to build a Free f a. We can do that if we can build a b, given alg :: f b -> b and k :: a -> b. So we can apply alg to ff if we can map every Free f a it contains to a b, but that's exactly what rightAdjunct does with alg and k.

As you might have guessed, this Free f is the free monad on the functor f (the church encoded version to be precise.)

instance Functor f => Monad (Free f) where
  return = unit
  m >>= f = rightAdjunct freeAlg f m
like image 154
Sjoerd Visscher Avatar answered Oct 06 '22 03:10

Sjoerd Visscher