Agda中的递归方案

Question

Agda中的递归方案

haskellrecursionagdacatamorphismrecursion-schemes

14

不用说，在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中编码递归方案？已经完成了吗？需要什么条件？

- luqui

4

今年的POPL会议上有一场有关在Coq中编码Data Types à la Carte的演示。他们描述了Fix结构的一个适用于Coq的替代方案，但我必须承认我还没完全理解它。这是他们实现的链接：http://www.cs.utexas.edu/~bendy/MTC/index.php - Mikhail Glushenkov

1

元理论 à la Carte 页面已经迁移到 http://people.csail.mit.edu/bendy/MTC/。 - Steven Shaw

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- copumpkin · Accepted Answer

您可以在Ulf Norell的经典Agda教程中找到这样的发展（在一个有限的函子宇宙中）！不幸的是，并非所有通常的递归方案都能够真正编码，因为所有“破坏性”的方案都会消耗数据，而所有“构造性”的方案都会产生协同数据，所以将一个方案馈送到另一个方案中的概念必然是不完全的。您可能可以在部分性Monad中完成所有操作，但这相当不令人满意。这基本上就是范畴论者所做的事情，他们说Haskell的“真实范畴”是CPO⊥，因为它的初始代数和终端余代数是一致的。