如何有效地将归纳类型转换为共感类型(无递归)？

Question

> {-# 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是双重的.作为归纳和coinductive数据类型的示例,请查看此仿函数.

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

没有递归,Ind StringF是一个有限的字符串,CoInd StringF是一个有限或无限的字符串(如果我们使用递归,它们都是有限的或无限的或未定义的字符串).通常,可以转换Ind f -> CoInd f任何Functor f.例如,我们可以围绕coinductive类型包含仿函数值

> 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)由于嵌套的Maybes,使得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 f的cowrap和Ind 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'从不直接或间接地使用递归.漂亮,不是吗!

Answer 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

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