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

  • A+
Category:Languages

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?

 


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.

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: