Defining Free Bind in a way that is compatible with the Free Monad

Question

So we have the free monad: (encoding may vary, but they're all the same)

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

instance Functor f => Monad (Free f) where
    pure = Pure
    Pure   x >>= f = f x
    Impure x >>= f = Impure ((>>= f) <$> x)

liftFree :: Functor f => f a -> Free f a
liftFree x = Impure (Pure <$> x)

runFree :: Monad g => (forall x. f x -> g x) -> Free f a -> g a
runFree _ (Pure   x) = pure x
runFree f (Impure x) = join (runFree f <$> f x)

such that runFree forms a monad homomorphism, which is the defining property of the free monad.

runFree f (pure x) = pure x
runFree f (liftFree x >>= liftFree . g) = f x >>= (f . g)
-- + some other associativity requirements

We can also make a similar construction to (what I believe to be) the free Bind from semigroupoids, which is a functor with only bind >>-:

data Free1 f a = Done (f a)
               | More (f (Free1 f a))

instance Functor f => Bind (Free f) where
    Done x >>- f = More (f <$> x)
    More x >>- f = More ((>>- f) <$> x)

liftFree1 :: f a -> Free1 f a
liftFree1 = Done

runFree1 :: Bind g => (forall x. f x -> g x) -> Free1 f a -> g a
runFree1 f (Done x) = f x
runFree1 f (More x) = f x >>- runFree1 f

and we get the appropriate bind homomorphism:

such that runFree1 forms a bind homomorphism, which is the defining property:

runFree1 f (liftFree1 x >>- liftFree1 . g) = f x >>- (f . g)
-- + some associativity laws

Now, these two types are great. We can convert from Free1 to Free, which makes sense:

toFree :: Free1 f a -> Free f a
toFree (Done x) = Impure (Pure   <$> x)
toFree (More x) = Impure (toFree <$> x)

but converting backwards is trickier. To go from a Free to a Free1, we would have to handle two cases:

1. The Free is pure, so cannot be represented in Free1.
2. The Free is impure, so can be represented in Free1.

It makes sense that these two cases can be handled statically, since we can just match on Pure or Impure.

So a reasonable type signature might be:

fromFree :: Functor f => Free f a -> Either a (Free1 f a)

but I am having problems writing this.

fromFree :: Free f a -> Either a (Free1 f a)
fromFree (Pure   x) = Left x   -- easy
fromFree (Impure x) = Right ?? -- a bit harder

It looks like the main problem is that we need to decide whether or not to use the Done or the More constructor without ever "running" the f. We need a:

f (Free f a) -> Free1 f a

which sounds like it might be troublesome for functors were you can't "get out", like IO.

So, this sounds impossible, unless I'm missing something.

There's another encoding that I've tried:

data Free1 f a = Free1 (f (Free f a))

this does lets us define fromFree, and it borrows from the NonEmpty construction (data NonEmpty a = a :| [a]). And I was able to use this approach when defining the "free Apply", which was nice. This does let us write toFree, fromFree, liftFree1, and a Bind instances. However, I can't seem to write runFree1:

runFree1 :: Bind g => (forall x. f x -> g x) -> f (Free f a) -> g a

as soon as I do anything, I seem to require return :: a -> g a, but we don't have this for all Bind g (I found a possible version that typechecks, but it performs the effects twice and so is not a proper bind homomorphism)

So, while this method gives us fromFree, I can't seem to find a way to write runFree1, which is the very thing that gives it "free Bind" capabilities.

Of these two methods, either we:

1. Have an actual free Bind with runFree1, but it is imcompatible with Free in that you can't "match" a Free into either a Free1, or a pure value.
2. Have a type that is compatible with Free (maybe a "nonempty Free"), but is not actually a free Bind (no runFree1), and defeats the whole purpose.

From this I can make one of two conclusions:

1. There is some way to make a free Bind Free1 that is compatible with Free, but I have not been able to figure it out yet
2. Fundamentally, we cannot have a free Bind that is compatible with Free. This seems to contradict my intuition (we can always immediately decide if a Free is pure or impure, so we should also be able to immediately distinguish between pure (zero effects) or Free1), but maybe there is a deeper reason that I am missing out on?

Which of these is the case? If #1, what is way, and if #2, what is the deeper reason? :)

Thank you in advance!

---

Edit To dispel my uncertainty about whether or not I was working with a "true Free Bind", I started looking at one that was truly a Free Bind by definition:

newtype Free1 f a = Free1 { runFree1 :: forall g. Bind g => (forall x. f x -> g x) -> g a }

And I can't seem to be able to write fromFree for this one, either. In the end I seem to need a g (Either a (Free1 a)) -> g a.

If I can't write fromFree for this, then it stands to reason that I can't write fromFree for any implementation of the free bind, since all implementations are isomorphic to this one.

Is there a way to write fromFree for this one, even? Or is it all impossible :'( It all worked so well for Alt/Plus and Apply/Applicative.

Answer 1

While Free f a is the type of trees with "f-nodes" and a-leaves, the "free Bind-structure" Free1 f a is the type of such trees with an additional restriction: the children of an f-node are either all leaves or all f-nodes. Thus if we consider binary trees:

data Bin x = Bin x x

Then Free Bin a contains the following tree shape, but Free1 Bin a does not:

Impure (Bin
  (Pure a)
  (Impure (Bin (Pure a) (Pure a))))

because the root node has one leaf and one Bin node as children, while a Free1 Bin a should have either two leaves, or two Bin nodes. Such a pattern could occur deep in a Free tree, so even a partial conversion Free f a -> Maybe (Free1 f a) is not possible with only a Functor f constraint. A Traversable f constraint with an assumption that the traversals are finite makes that conversion possible, but of course it's still not practical for large trees since they must be fully traversed before any output can be produced.

Note that because of the above characterization of Free1, this other definition in terms of Free is not actually equivalent:

data Free1 f a = Free1 (f (Free f a))  -- Not a free Bind