流软件包的流数据类型是否等同于FreeT？
data Stream f m r
= Step !(f (Stream f m r))
| Effect (m (Stream f m r))
| Return r关于Stream类型的注释如下所示：
Stream数据类型等同于FreeT，可以表示任何有效的连续步骤，其中步骤或“命令”的形式由第一个(函数器)参数指定。
我想知道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即使看起来不可能在FreeT之间创建同构，Stream也可以被认为等同于FreeT吗？
回答 2
Stack Overflow用户
发布于 2018-05-30 00:19:48
有一些小的差异使得它们在字面上不是等价的。特别是，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)请注意用于扁平化多个Effect构造函数的go循环。
防伪：(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)))Case 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 quotientCase 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向左对话作为练习。
Stack Overflow用户
发布于 2018-05-30 01:01:38
您的Return示例和我的嵌套Effect构造函数示例都不能用具有相同参数f和m的FreeT表示。还有更多的反例。数据类型之间的潜在差异最能在手写空间中看到，在这个空间中，数据构造函数被剥离，并且允许无限类型。
Stream f m a和FreeT f m a都用于将a类型嵌套在一堆f和m类型构造函数中。Stream允许任意嵌套f和m，而FreeT则更加严格。它总是有一个外部m。它包含一个f和另一个m并重复，或者包含一个a并终止。
但这并不意味着这两种类型之间没有某种等价性。您可以通过证明每种类型都可以忠实地嵌入到另一种类型中来显示某种等价性。
在FreeT中嵌入Stream可以在一个观察的基础上完成:如果您选择一个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中。
我要说的是，这使得文档是正确的，尽管它可能应该使用比“等效”更精确的术语。可以用一种类型构造的任何东西，都可以用另一种类型构造--但可能会对嵌入进行一些额外的解释，并涉及到变量的更改。
https://stackoverflow.com/questions/50585417
复制相似问题