流媒体包的Stream数据类型是否等同于FreeT？

Question

该流包定义Stream类型,看起来像下面这样:

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

对Stream类型的评论说明如下:

的Stream数据类型是等同于FreeT,并且可以表示的步骤,其中,通过所述第一(算符)参数指定的步骤或"命令"形式的任何effectful继承.

我想知道这种Stream类型是怎样的FreeT？

这是以下定义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)) }

看起来不可能在这两种类型之间创建同构.

具体来说,我没有找到一种方法来编写以下两个使它们成为同构的函数:

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

举例来说,我不知道怎么表达的值一样Return "hello" :: Stream f m String的FreeT.

我想它可以像下面那样完成,但是Pure "hello"必须包含在一个中m,而Return "hello" :: Stream f m String它不是:

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

---

可以Stream被视为等同于FreeT,即使不出现可能创建它们之间的同构？

Answer 1

存在一些细微的差异，使得它们在字面上并不等同。特别是，强制执行和FreeT的交替，fm

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

而Stream允许口吃，例如，我们可以构造以下Step两个之间没有 no 的内容Effect：

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

在某种意义上应该相当于

Return r

因此，我们将通过以下方程取商Stream，使 的各层变平Effect：

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

在该商下，以下是同构

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)

请注意go用于展平多个Effect构造函数的循环。

伪防伪：(freeT_stream . stream_freeT) = id

我们对流进行归纳x。老实说，我是凭空提出归纳假设的。当然存在归纳法不适用的情况。这取决于 和m是f什么，并且可能还存在一些重要的设置来确保这种方法对于商类型有意义。但应该还有很多具体的内容m以及f该方案适用的地方。我希望有一些明确的解释可以将这个伪证明转化为有意义的东西。

(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)))

案例x = Step f，归纳假设（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

案件x = Return r

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

案例x = Effect m,归纳假设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

向左交谈作为练习。