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

Question

streaming package defines a Stream 类型如下所示：

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

Stream 类型的评论如下：

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.

我想知道 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 强制交替使用 f 和 m、

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

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

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

匡威作为练习。

Answer 2

你的 Return 示例和我的嵌套 Effect 构造函数的示例都不能由具有相同参数 f 和 m 的 FreeT 表示。还有更多的反例。数据类型的潜在差异可以在手波 space 中最好地看出，其中数据构造函数被剥离并允许无限类型。

Stream f m a 和 FreeT f m a 都是为了在一堆 f 和 m 类型构造函数中嵌套一个 a 类型。 Stream 允许 f 和 m 的任意嵌套，而 FreeT 则更严格。它总是有一个外部 m。它包含一个 f 和另一个 m 并重复，或者包含一个 a 并终止。

但这并不意味着类型之间没有某种等价性。您可以通过证明每种类型都可以忠实地嵌入另一种类型来证明某种等价性。

将 Stream 嵌入 FreeT 可以在一个观察的背后完成：如果您选择 f' 和 m' 这样 f 和 m 类型构造函数在每个级别都是可选的，您可以建模 f 和 m 的任意嵌套。一种快速的方法是使用 Data.Functor.Sum，然后编写一个函数：

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

请注意，该类型将没有运行所需的实例。这可以通过将 Sum Identity 切换到实际上具有适当 Monad 实例的更直接的类型来纠正。

反向转换不需要任何类型更改技巧。 FreeT 更受限制的形状已经可以直接嵌入到 Stream.

中

我会说这使文档正确，但可能它应该使用比 "equivalent" 更精确的术语。任何你可以用一种类型构造的东西，你都可以用另一种类型构造——但可能对嵌入和所涉及的变量变化有一些额外的解释。

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

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

haskell

stream

monad-transformers

free-monad