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