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的规范Agda教程中找到这样一个开发(在一个有限的仿函数范围内)!

遗憾的是,并非所有通常的递归方案都可以真正编码,因为所有"破坏性"的递归方案都会消耗数据,而所有"建构"的方法都会产生密码数据,因此将一个进给到另一个的概念必然是部分的.你可能可以在偏好monad中完成所有这些但是相当不令人满意.当他们说Haskell的"真正的类别"是CPO⊥时,这或多或少是分类者正在做的事情,因为它的最初代数和终端余代数是重合的.