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.