> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-}
任何归纳类型的定义如下所示
> newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r}
> induction = flip flipinduct
归纳法的类型为(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是一个有限或无限的字符串（如果我们使用递归，它们都可以是有限的、无限的或未定义的字符串）。一般来说，可以将任何Functor f转换为Ind f -> CoInd 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)
归纳法的时间复杂度始终为O(n)，因此cowrap的时间复杂度也是O(n)。
我们可以使用协同归纳法从cowrap和归纳法产生CoInd f。
> convert' :: (Functor f) => Ind f -> CoInd f
> convert' = coinduction cowrap
每当我们获取一个元素，这又是 O(n) 的操作, 总共需要进行 O(n^2) 次.
我的问题是，不使用递归（直接或间接），我们能否在 O(n) 的时间内将 Ind f 转换为 CoInd f？
我知道如何使用递归来完成此操作（将 Ind f 转换为 Fix f 然后再将 Fix f 转换为 CoInd f （初始转换的复杂度为 O(n)，但却是每个来自 CoInd f 的元素都是 O(1), 使得第二次转换总时间复杂度为 O(n)，而 O(n) + O(n) = O(n) ）），但我想看看是否有没有递归的方法。
请注意，convert 和 convert' 从未使用递归，直接或间接地。真是巧妙，不是吗！
f :: f a -> a，cata f:: Mu f -> a 是从初始f-代数（Mu f）到a的唯一的f-代数同态。这就是你得到(f a -> a) -> Mu f -> a的方式。将其翻转并可将其作为Mu f的定义！关于ana / coinduction，给定一个f-余代数（f :: a -> f a），我们有ana f :: a -> Nu f。因此，(a -> f a) -> a -> Nu f。被翻转的箭头是'f'和cata f/ana f箭头，而不是元理论中的箭头。当你对单子的定义进行对偶以构造余单子时，同样的事情会发生。 - Edward Kmettmap，它是这样的：map = reverse . map' [] where {map' seed [] = seed; map' seed (x : xs) = map' (x : seed) xs}。 - dfeuer