15 
> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-}

任何归纳类型都是这样定义的

> newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r}
> induction = flip flipinduct

induction有类型(f a -> a) -> Ind f -> a。这有一个双重概念，称为共导。

> data CoInd f = forall r. Coinduction (r -> f r) r
> coinduction = Coinduction

coinduction有类型(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为任何 Functor 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)，但第 n 个元素是O(n)由于嵌套Maybe的 s 造成的，因此是O(n^2)总数。）对偶，我们可以定义cowrap，它采用归纳类型，并显示其顶部 Functor 层。

> 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生产。CoInd fcowrapInd f

> convert' :: (Functor f) => Ind f -> CoInd f
> convert' = coinduction cowrap

每次我们获得一个元素时都会再次出现这种情况O(n)，总共O(n^2).

我的问题是，不使用递归（直接或间接），我们可以及时Ind f转换吗？CoInd fO(n)

我知道如何使用递归（先转换为Ind f，然后Fix f再转换Fix f为CoInd f（初始转换为O(n)CoInd fO(1)O(n)O(n) + O(n) = O(n)

观察这一点convert，convert'从不直接或间接使用递归。漂亮，不是吗！

4

1 回答 1

1

是的，这在形式上是可能的：

https://github.com/jyp/ControlledFusion/blob/master/Control/FixPoints.hs

但是，转换仍然需要在运行时构建一个中间缓冲区，这只能使用循环来完成。

这种限制的原因是“归纳”类型的值响应给定的评估顺序 (*)，而“共同归纳”类型的值固定了评估顺序。在不强制进行许多重新计算的情况下使转换成为可能的唯一方法是分配某种中间缓冲区，以记忆中间结果。

顺便说一句，从“共归纳”到“归纳”的转换不需要缓冲，但需要通过使用显式循环来重新定义评估顺序。

顺便说一句，我在两篇论文中研究了基本概念：1.在 Haskell 中，对于有效的流：https ://gist.github.com/jyp/fadd6e8a2a0aa98ae94d 2.在经典线性逻辑中，对于数组和流。http://lopezjuan.com/limestone/vectorcomp.pdf

(*) 这是假设一种严格的语言。存在惰性评估时情况会有所变化，但概念和最终答案是相同的。源代码中有一些关于惰性求值的注释。

于 2015-12-10T21:19:54.920 回答