13

言うまでもなく、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 で再帰スキームをエンコードする希望はありますか? それは行われましたか？何が必要ですか？

4

1 に答える 1

17

Ulf Norell の正規の Agda チュートリアルで、(制限されたファンクターの宇宙での) そのような開発を見つけることができます!

残念ながら、すべての通常の再帰スキームを実際にエンコードできるわけではありません。これは、すべての「破壊」スキームがデータを消費し、すべての「構築」スキームがコードデータを生成するためです。おそらく部分モナドですべてを行うことができますが、それはかなり不十分です。Haskell の「真の圏」が CPO⊥ であると彼らが言うとき、それは多かれ少なかれ圏論者がしていることです。

于 2013-02-05T02:46:44.343 に答える