haskell - 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 中找到这样的发展(在有限的仿函数范围内)。 !

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