9

Haskell のリストは次のようになります。

data List a = Nil | Cons a (List a)

型理論の解釈は次のとおりです。

λα.μβ.1+αβ

リスト型をファンクターの固定小数点としてエンコードします。Haskell では、これを次のように表すことができます。

data Fix f = In (f (Fix f))
data ListF a b = Nil | Cons a b
type List  a   = Fix (ListF a)

先ほどのμバインダーの範囲が気になります。外側のスコープにバインドされた名前は、内側のスコープで引き続き使用できますか? たとえば、次の式は有効ですか。

μγ.1+(μβ.1+γβ)γ

...おそらく次と同じです：

μβ.μγ.1+(1+γβ)γ

...しかし、名前が再利用されると、どのように変化しますか:

μβ.μγ.1+(μβ.1+γβ)γ

上記はすべてレギュラータイプですか？

4

2 に答える 2

9

μ のスコープは他のバインダーと同じように機能するため、はい、すべての例が有効です。また、λ が含まれていないため、規則的でもあります。(*)

平等に関しては、それはあなたがどのような種類のμタイプを持っているかによって異なります. 基本的に 2 つの異なる概念があります。

  • equi-recursive : その場合、型付け規則は等価性を仮定します

    μα.T = T[μα.T / α]

    つまり、再帰型は、その 1 レベルの「展開」に等しいと見なされます。ここでは、μ が削除され、μ にバインドされた変数が型自体に置き換えられます (この規則は繰り返し適用できるため、任意の回数展開できます)。 ）。

  • iso-recursive : ここでは、そのような等価物は存在しません。代わりに、μ-type は、それを導入および排除するための独自の表現形式を持つ別個の形式の型です。これらは通常、ロールとアンロール (またはフォールドとアンフォールド) と呼ばれ、次のように型付けされます。

    ロール : T[μα.T / α] → μα.T

    unroll : μα.T → T[μα.T / α]

    これらは、上記の方程式を反映するために用語レベルで明示的に適用する必要があります (展開の各レベルに対して 1 回)。

ML や Haskell などの関数型言語は、通常、データ型の解釈に後者を使用します。ただし、ロール/アンロールは、データ コンストラクターの使用に組み込まれています。したがって、各コンストラクターは、合計型への注入で構成された iso-recursive 型への注入です (一致する場合は逆になります)。

あなたの例は、等再帰的な解釈ではすべて異なります。最初と 3 番目は等再帰的解釈の下では同じです。これは、上記の等価性を適用すると外側の μ が消えるだけだからです。

(*) 編集: 不規則再帰型とは、無限展開が通常のツリーに対応しない (または同等に、有限巡回グラフで表すことができない) 型です。このような場合は、再帰型コンストラクター、つまり、μ の下で発生する λ でのみ表現できます。たとえば、μα.λβ.1+α(β×β) -- 再帰方程式 t(β) = 1+t(β×β) に対応する -- は、再帰型コンストラクター α が再帰的に適用されるため、不規則になります。その引数よりも「大きい」型に変換されるため、すべてのアプリケーションは無限に「成長」する再帰型です (したがって、グラフとして描画することはできません)。

ただし、μ を使用したほとんどの型理論では、その束縛変数は基底の種類に制限されているため、不規則な型をまったく表現できないことに注意してください。特に、制限のない等再帰型コンストラクターを使用する理論では、非終了の型正規化が行われるため、型の等価性 (したがって型チェック) は決定できません。等再帰型の場合、高次のロール/アンロールが必要になりますが、これは可能ですが、それを調査している文献はあまり知りません。

于 2014-03-22T08:48:14.690 に答える
8

型式μは有効です。再帰、合計、および積のみを使用するため、型も規則的であると思います。

タイプ

T1 = μγ.1+(μβ.1+γβ)γ

に等しく見えません

T2 = μβ.μγ.1+(1+γβ)γ

2 番目のタイプがinr (inr (inl *, inr (inl *)), inl *)ありますが、最初のタイプはありません。

最後のタイプ

T3 = μβ.μγ.1+(μβ.1+γβ)γ

は (最初の β を α 変換) に等しい

μ_.μγ.1+(μβ.1+γβ)γ

つまり、トップレベルの μ を展開します。

μγ.1+(μβ.1+γβ)γ

ですT1。

基本的に、μ 束縛変数のスコープは、λ 束縛変数と同じ規則に従います。つまり、変数の各オカレンスの値は、その上に最も近いβものによって提供されます。 μβ

于 2014-03-21T23:23:01.247 に答える