haskell - 流包的Stream数据类型是否等同于FreeT？

Question

streaming包定义了 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 = 步骤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 = 返回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

<小时/>

将左对话作为练习。