如何有效地将归纳类型转换为共归纳类型（无需递归）？

Question

> {-# 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

共感应具有(a->f a)->a->CoInd f类型。注意归纳和共归纳是如何对偶的。作为归纳和共归纳数据类型的示例，请看这个函式。

> data StringF rec = Nil | Cons Char rec deriving Functor

> 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

> convert :: (Functor f) => Ind f -> CoInd f
> convert = induction wrap

> 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也是如此。

我们可以使用cointension从cowrap和ind f生成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转换为O(n)（初始转换是O(n)，但随后coind f)中的每个元素都是O(1)，使得第二次转换O(n)total和O(n)+O(n)=O(n))，但我想看看是否可以不这样做。

注意convert和convert'从未直接或间接地使用递归。很漂亮，不是吗！

Answer 1

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

https://github.com/jyp/controlledfusion/blob/master/control/fixpoints.hs

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