Is the streaming package's Stream data type equivalent to FreeT?

Question

The streaming package defines a Stream type that looks like the following:

data Stream f m r
  = Step !(f (Stream f m r))
 | Effect (m (Stream f m r))
 | Return r

There is a comment on the Stream type that says the following:

The Stream data type is equivalent to FreeT and can represent any effectful succession of steps, where the form of the steps or 'commands' is specified by the first (functor) parameter.

I'm wondering how the Stream type is equivalent to FreeT?

Here is the definition of FreeT:

data FreeF f a b = Pure a | Free (f b)
newtype FreeT f m a = FreeT { runFreeT :: m (FreeF f a (FreeT f m a)) }

It looks like it is not possible to create an isomorphism between these two types.

To be specific, I don't see a way to write the following two functions that makes them an isomorphism:

freeTToStream :: FreeT f m a -> Stream f m a
streamToFreeT :: Stream f m a -> FreeT f m a

For instance, I'm not sure how to express a value like Return "hello" :: Stream f m String as a FreeT.

I guess it could be done like the following, but the Pure "hello" is necessarily going to be wrapped in an m, while in Return "hello" :: Stream f m String it is not:

FreeT $ pure $ Pure "hello" :: Applicative m => FreeT f m a

---

Can Stream be considered equivalent to FreeT even though it doesn't appear possible to create an isomorphism between them?

Answer 1

There are some small differences that make them not literally equivalent. In particular, FreeT enforces an alternation of f and m,

FreeT f m a = m (Either a (f (FreeT f m a) = m (Either a (f (m (...))))
                                          -- m            f  m  -- alternating

whereas Stream allows stuttering, e.g., we can construct the following with no Step between two Effect:

Effect (return (Effect (return (Return r))))

which should be equivalent in some sense to

Return r

Thus we shall take a quotient of Stream by the following equations that flatten the layers of Effect:

Effect (m >>= \a -> return (Effect (k a))) = Effect (m >>= k)
Effect (return x) = x

Under that quotient, the following are isomorphisms

freeT_stream :: (Functor f, Monad m) => FreeT f m a -> Stream f m a
freeT_stream (FreeT m) = Effect (m >>= \case
  Pure r -> return (Return r)
  Free f -> return (Step (fmap freeT_stream f))

stream_freeT :: (Functor f, Monad m) => Stream f m a -> FreeT f m a
stream_freeT = FreeT . go where
  go = \case
    Step f -> return (Free (fmap stream_freeT f))
    Effect m -> m >>= go
    Return r -> return (Pure r)

Note the go loop to flatten multiple Effect constructors.

---

Pseudoproof: (freeT_stream . stream_freeT) = id

We proceed by induction on a stream x. To be honest, I'm pulling the induction hypotheses out of thin air. There are certainly cases where induction is not applicable. It depends on what m and f are, and there might also be some nontrivial setup to ensure this approach makes sense for a quotient type. But there should still be many concrete m and f where this scheme is applicable. I hope there is some categorical interpretation that translates this pseudoproof to something meaningful.

(freeT_stream . stream_freeT) x
= freeT_stream (FreeT (go x))
= Effect (go x >>= \case
    Pure r -> return (Return r)
    Free f -> return (Step (fmap freeT_stream f)))

Case x = Step f, induction hypothesis (IH) fmap (freeT_stream . stream_freeT) f = f:

= Effect (return (Step (fmap freeT_stream (fmap stream_freeT f))))
= Effect (return (Step f))  -- by IH
= Step f  -- by quotient

Case x = Return r

= Effect (return (Return r))
= Return r   -- by quotient

Case x = Effect m, induction hypothesis m >>= (return . freeT_stream . stream_freeT)) = m

= Effect ((m >>= go) >>= \case ...)
= Effect (m >>= \x' -> go x' >>= \case ...)  -- monad law
= Effect (m >>= \x' -> return (Effect (go x' >>= \case ...)))  -- by quotient
= Effect (m >>= \x' -> (return . freeT_stream . stream_freeT) x')  -- by the first two equations above in reverse
= Effect m  -- by IH

---

Converse left as an exercise.

Answer 2

Both your example with Return and my example with nested Effect constructors cannot be represented by FreeT with the same parameters f and m. There are more counterexamples, too. The underlying difference in the data types can best be seen in a hand-wavey space where the data constructors are stripped out and infinite types are allowed.

Both Stream f m a and FreeT f m a are for nesting an a type inside a bunch of f and m type constructors. Stream allows arbitrary nesting of f and m, while FreeT is more rigid. It always has an outer m. That contains either an f and another m and repeats, or an a and terminates.

But that doesn't mean there isn't an equivalence of some sort between the types. You can show some equivalence by showing that each type can be embedded inside the other faithfully.

Embedding a Stream inside a FreeT can be done on the back of one observation: if you choose an f' and m' such that the f and m type constructors are optional at each level, you can model arbitrary nesting of f and m. One quick way to do that is use Data.Functor.Sum, then write a function:

streamToFreeT :: Stream f m a -> FreeT (Sum Identity f) (Sum Identity m) a
streamToFreeT = undefined -- don't have a compiler nearby, not going to even try

Note that the type won't have the necessary instances to function. That could be corrected by switching Sum Identity to a more direct type that actually has an appropriate Monad instance.

The transformation back the other direction doesn't need any type-changing trickery. The more restricted shape of FreeT is already directly embeddable inside Stream.

I'd say this makes the documentation correct, though possibly it should use a more precise term than "equivalent". Anything you can construct with one type, you can construct with the other - but there might be some extra interpretation of the embedding and a change of variables involved.