なぜ帰納的データ型では、型の再帰が -> の前で発生する `data Bad a = C (Bad a -> a)` のような型を禁止するのでしょうか?

Question

Agdaマニュアルについて 帰納的データ型とパターン マッチング 状態:

正規化を確実に行うには、帰納的出現が厳密に正の位置に現れる必要があります。たとえば、次のデータ型は許可されません。

data Bad : Set where
  bad : (Bad → Bad) → Bad

コンストラクターへの引数に Bad の否定的な出現があるためです。

帰納的データ型にこの要件が必要なのはなぜですか?

Answer 1

指定したデータ型は、 型なし ラムダ計算。

data Bad : Set where
  bad : (Bad → Bad) → Bad

unbad : Bad → (Bad → Bad)
unbad (bad f) = f

方法を見てみましょう。型なしラムダ計算には次の用語があることを思い出してください。

 e := x | \x. e | e e'

翻訳を定義できます [[e]] 型なしラムダ計算項から型の Agda 項へ Bad (Agda ではありませんが):

[[x]]     = x
[[\x. e]] = bad (\x -> [[e]])
[[e e']]  = unbad [[e]] [[e']]

これで、お気に入りの非終了の型なしラムダ項を使用して、型の非終了項を生成できるようになりました。 Bad. 。たとえば、次のように翻訳できます。 (\x. x x) (\x. x x) type の非終了式へ Bad 下に：

unbad (bad (\x -> unbad x x)) (bad (\x -> unbad x x))

この型はたまたまこの引数にとって特に便利な形式でしたが、少しの作業で負の再帰が発生する任意のデータ型に一般化できます。

Answer 2

このようなデータ型により、どのような型でも生息できるようになる例が、D.A. ターナーに示されています。(2004-07-28)、 トータル関数型プログラミング, 、宗派。3.1、758 ページ ルール 2:型再帰は共変でなければなりません."

---

Haskell を使用して、より複雑な例を作成してみましょう。「悪い」再帰データ型から始めます

data Bad a = C (Bad a -> a)

そして構築します Y コンビネータ 他の形式の再帰なしでそこから。これは、そのようなデータ型を使用すると、あらゆる種類の再帰を構築したり、無限再帰によってあらゆる型を常駐させたりできることを意味します。

型なしラムダ計算の Y コンビネータは次のように定義されます。

Y = λf.(λx.f (x x)) (λx.f (x x))

その鍵となるのは、私たちが応用することです x 自分自身に x x. 。型付き言語では、有効な型が存在しないため、これは直接不可能です。 x あるかもしれない。しかし、私たちの Bad データ型では、このモジュロでコンストラクターを追加/削除できます。

selfApp :: Bad a -> a
selfApp (x@(C x')) = x' x

取る x :: Bad a, 、コンストラクターをアンラップして、内部の関数を適用できます。 x 自体。これを行う方法がわかれば、Y コンビネータを簡単に構築できます。

yc :: (a -> a) -> a
yc f =  let fxx = C (\x -> f (selfApp x))  -- this is the λx.f (x x) part of Y
        in selfApp fxx

ご了承ください どちらでもない selfApp または yc は再帰的ですが、関数自体への再帰呼び出しはありません。 再帰は、再帰データ型でのみ表示されます。

構築されたコンビネータが実際に期待どおりの動作をしていることを確認できます。無限ループを作ることができます。

loop :: a
loop = yc id

あるいは計算してみましょう GCD:

gcd' :: Int -> Int -> Int
gcd' = yc gcd0
  where
    gcd0  :: (Int -> Int -> Int) -> (Int -> Int -> Int)
    gcd0 rec a b  | c == 0     = b
                  | otherwise  = rec b c
      where c = a `mod` b