相关疑难解决方法(0)

毋庸置疑,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编码递归方案有什么希望吗？它完成了吗？需要什么？