如何有效地将归纳类型转换为共归纳类型(不需要递归)？
> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-}任何归纳类型的定义如下
> newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r}
> induction = flip flipinductinduction的类型为(f a -> a) -> Ind f -> a。这有一个双重概念，叫做共归纳。
> data CoInd f = forall r. Coinduction (r -> f r) r
> coinduction = Coinductioncoinduction的类型为(a -> f a) -> a -> CoInd f。注意induction和coinduction是双重的。作为归纳和共归纳数据类型的一个例子，请看这个函子。
> data StringF rec = Nil | Cons Char rec deriving Functor没有递归，Ind StringF是有限字符串，CoInd StringF是有限字符串或无限字符串(如果使用递归，它们都是有限的、无限的或未定义的字符串)。通常，可以将Ind f -> CoInd f转换为任何函子f。例如，我们可以将函子值封装在协归纳类型的周围。
> wrap :: (Functor f) => f (CoInd f) -> CoInd f
> wrap fc = coinduction igo Nothing where
> --igo :: Maybe (CoInd f) -> f (Maybe (CoInd f))
> igo Nothing = fmap Just fc
> igo (Just (Coinduction step seed)) = fmap (Just . Coinduction step) $ step seed此操作为每个步骤添加一个额外的操作(模式匹配Maybe)。这意味着它会给O(n)带来开销。
我们可以在Ind f和wrap上使用归纳法得到CoInd f。
> convert :: (Functor f) => Ind f -> CoInd f
> convert = induction wrap我是O(n^2)。(获取第一个层的是O(1)，但是由于嵌套的Maybe，第n个元素是O(n)，这使得O(n^2)总数。)在对偶上，我们可以定义cowrap，它是一种归纳类型，并揭示了它的顶层函子层。
> cowrap :: (Functor f) => Ind f -> f (Ind f)
> cowrap = induction igo where
> --igo :: f (f (Ind f)) -> f (Ind f)
> igo = fmap (\fInd -> Ind $ \fold -> fold $ fmap (`flipinduct` fold) fInd)induction总是O(n)，cowrap也是。
我们可以使用coinduction从cowrap和Ind f中产生CoInd f。
> convert' :: (Functor f) => Ind f -> CoInd f
> convert' = coinduction cowrap每次我们得到一个元素时，这都是O(n)，总共是O(n^2)。
我的问题是，在不使用递归(直接或间接)的情况下，我们能否在Ind f时将CoInd f转换为O(n)时间？
我知道如何使用递归(将Ind f转换为Fix f，然后将Fix f转换为CoInd f )(最初的转换是O(n)，但CoInd f中的每个元素都是O(1)，从而使第二个转换O(n)总计，以及O(n) + O(n) = O(n))，但我想看看它是否可能没有。
观察到convert和convert'从未直接或间接地使用递归。好极了，不是吗！
回答 1
Stack Overflow用户
发布于 2015-12-10 21:19:54
是的，这在形式上是可能的：
https://github.com/jyp/ControlledFusion/blob/master/Control/FixPoints.hs
但是，转换仍然需要在运行时构造一个只能使用循环完成的中间缓冲区。
造成这种限制的原因是，“归纳”类型的值响应于给定的计算顺序(*)，而“共归纳”类型的a值则确定了计算的顺序。在不需要进行多次重新计算的情况下，使过渡成为可能的唯一方法是分配某种中间缓冲区，回溯中间结果。
顺便说一句，从“共归纳”到“归纳”的转换不需要缓冲，但需要使用显式循环来重新定义计算顺序。
顺便说一下，我在两篇论文中研究了基本概念: 1.在Haskell中，对于有效流：https://gist.github.com/jyp/fadd6e8a2a0aa98ae94d 2。在经典线性逻辑中，数组和流。http://lopezjuan.com/limestone/vectorcomp.pdf
(*)这是一种严格的语言。在懒散的评估中，事情会发生一些变化，但概念和最终答案是一样的。在源代码中有一些关于延迟计算的注释。
https://stackoverflow.com/questions/34123543
复制相似问题
腾讯云开发者
