Agda 中的递归方案

Question

不用说，Haskell 中的标准构造

newtype Fix f = Fix { getFix :: f (Fix f) }

cata :: (Functor f) => (f a -> a) -> Fix f -> a
cata f = f . fmap (cata f) . getFix 

很棒而且非常有用。

尝试在 Agda 中定义一个类似的东西（为了完整起见，我将把它放出来）

data Fix (f : Set -> Set) : Set where
    mkFix : f (Fix f) -> Fix f

失败是因为f 不一定是严格正数。这是有道理的——通过适当的选择，我可以很容易地从这个结构中得到一个矛盾。

我的问题是：有没有希望在 Agda 中编码递归方案？已经完成了吗？需要什么？

Answer 1

您会在Ulf Norell's canonical Agda tutorial 中找到这样的发展（在有限的函子范围内）！

不幸的是，并非所有常见的递归方案都可以真正编码，因为所有“破坏性”方案都会消耗数据，而所有“构造性”方案都会产生 codata，因此将一个输入另一个的概念必然是部分的。您可能可以在偏心单子中完成所有操作，但这并不令人满意。当分类学家说 Haskell 的“真实范畴”是 CPO⊥ 时，这或多或少是这样做的，因为它的初始代数和终端代数重合。