rank 2 types の勉強

先週、以下のように書きました。

  •  (\lambda x. x \ x)という項には、 (\forall X. X→X)→(\forall X. X→X)という型がつく
  •  (\lambda y.\lambda z. z)という項には \forall Y. Y→\forall Z. Z→Zという型がつく
  • これらを組み合わせても、 (\lambda x. x \ x)(\lambda y.\lambda z. z)の型検査を通すことができない
  • しかし、 (\lambda x. x \ x)(\lambda y.\lambda z. z)は、簡約が停止する

この矛盾がよくわからなかったのですが、詳しく調べたところ分かったので書いておきます。

 (\lambda x. x \ x)(\lambda y.\lambda z. z)の正しい型

この式に型をつけるためには、以下のようにすればよいことが分かります。

 \vdash (\lambda x. x \ x) : \forall K. \forall X. X→K

 \vdash (\lambda y.\lambda z. z) : \forall Y. Y→\forall Z. Z→Z

 \vdash (\lambda x. x \ x)(\lambda y.\lambda z. z) : \forall Z. Z→Z

どうやってこれを思いつくか

これは型再構築アルゴリズムではありませんが、私がどのようにこの型を思いついたかを書きます。

  1. 自己適用になっているので、単純型では型付け不能
  2. よって、 xはどんな型も受け取れる関数型になっている
  3. つまり、 x : \forall X. X→K(X)となるはず
  4. ここで、 K(X) Xに依存しない定数なら、 x : \forall X. X→K
  5.  xはこの型を受け取る関数なので、 Xを具体化して x : (\forall X. X→K)→K
  6. よって x \ x : K
  7. つまり、 (\lambda x. x \ x) : (\forall X. X→K)→K
  8.  Kは自由な型変数なので一般化して (\lambda x. x \ x) : \forall K. (\forall X. X→K)→K

ある項の型は一つとは限らない

ここが勘違いしていたところで、「ある項が型付け可能」といっても、その項が 複数の型を持つことはありうる ということです。実際、 (\lambda x. x \ x)は上で書いた K(X)を自由にとることで、無限に多くの種類の型をつけられることが分かります。

  •  (\lambda x. x \ x) : \forall K. (\forall X. X→K)→K
    •  K(X) = Kとした場合
    •  (\lambda y.\lambda z. z)などが受け取れる
  •  (\lambda x. x \ x) : (\forall X. X→X)→(\forall X. X→X)
    •  K(X) = Xとした場合
    •  (\lambda y. y)を受け取れる
  •  (\lambda x. x \ x) : \forall K. (\forall X. X→K→X)→K→(\forall X. X→K→X)
    •  K(X) = K→Xとした場合
    •  (\lambda y.\lambda z. y)を受け取れる
  • ……

主要型

 \lambda x. xも、無限に多くの種類の型、 Int→Int Bool→Bool (Int→Bool)→(Int→Bool)、……を持ちました。しかしこれらはいずれも X→Xを具体化したものになっています。このような、無限に多くの種類の型をつけられるけれど、実は全部「何か」を具体化したものになっている、という状況における「何か」を主要型と言います。

しかし、先に上げた無限に多くの種類の型は、何か一つの型を具体化したものになっている雰囲気がありません。実際、この項には主要型がありません。

普通は主要型のある体系を扱うため勘違いしていたのですが、 主要型のない体系もある ということです。System F はまさにそのような体系の例になっています。

つまり、System Fでは、 (\lambda x. x \ x)を(完全には)多相的に取り扱えないことになります。 (\lambda x. x \ x)を受け取る関数では、どういった型で受け取るかを事前に決める必要があるということです。

なお、主要型を定義するにはいかにも∀が必要な感じがありますが、実際には体系内にある必要はなくて、メタ的に使えればよいようです。このため、単純型付きラムダ計算は主要型を持ちます。

rank 2 types

このようなややこしい事態が発生するのは、多相関数を受け取るような関数が許されることによります。そういうことをしたい場合はそんなに多くないと言われています*1。ということは、「(多相関数を受け取る関数)を受け取る関数」なんていうものは実用上のプログラムではまず見かけないはずです。そういうのに型をつけることをあきらめ、多相関数を受け取る関数までしか許さない型体系は、rank 2 types と呼ばれます。

なぜ rank 2 に制限するのかというと、ここまでの範囲ならば型再構築が可能だからです。「(多相関数を受け取る関数)を受け取る関数」に型をつけるためにはrank 3 type が必要になりますが、これを許すと型再構築が決定不可能になります。

ちなみに、多くの実用的な型再構築を持つ言語は、rank 1 までの制限となっており、多相関数は許しても多相関数を受け取る関数は許されません。 rank 1 に制限しても型再構築アルゴリズムの時間計算量クラスはDEXPTIME完全のまま変わらないのですが……。

Intersection type(交差型)

型Tとしても取り扱え、型Sとしても取り扱える、みたいな型をT∧Sと交差型を使って表せます。全称型がパラメトリック多相(ジェネリクス)に対応するように、交差型はアドホック多相(オーバーロード)に対応するようです(単にそういう言語機能の解釈としても使えるというだけです。ラムダ計算にはオーバーロードのような機能はありません)。

交差型は多相を表現する、全称型ではない方法の一つです。上で書いたrank の話は、全称型だけではなく交差型にもあてはまります。

重要な事実は、以下の二点です。

  • rank 2 までの全称型システムを使って型をつけられる項の集合は、rank 2 までの交差型システムを使って型をつけられる項の集合に等しい
  • (rank 2 までの全称型システムには主要型が存在しない項もあるにもかかわらず)rank 2 までの交差型システムでは常に主要型が存在する

 (\lambda x. x \ x)の主要型

System F では、この項の主要型を表現できません。

一方、交差型システムでは rank 2 の範囲である以下の型が主要型になります。

 (\lambda x. x \ x) : (T \wedge (T→U))→U

驚くほど単純ですが、先の例を具体化したものは、いずれもこれを具体化したものになっていることが確かめられます。

  •  (\lambda x. x \ x) : (\forall X. X→K)→K
    •  U = K, T = (\forall X. X→K)
  •  (\lambda x. x \ x) : (\forall X. X→X)→(\forall X. X→X)
    •  U = (\forall X. X→X), T = (\forall X. X→X)
  •  (\lambda x. x \ x) : (\forall X. X→K→X)→K→(\forall X. X→K→X)
    •  U = K→(\forall X. X→K→X), T = (\forall X. X→K→X)

T, Uは任意のものが許されるため、System Fでつく型よりも広くなっている気もします。ただ、その項に属するラムダ項がないような型を受け取る関数としても具体化できるというのはSystem Fでもそうなので、あまり気にするべきことではないのでしょうか。

まとめ

  • 項に型がつくというのと、主要型があるというのは全く別の問題
  • System Fでは、主要型がないこともある
  • System of the intersection typeでは、常に主要型がある
  • rank 2 に制限した時、
    • 型をつけられる項の集合は全称型でも交差型でも同じ
    • しかし、主要型のある項の集合は交差型の方が真に大きい
      • 具体的な例は、 (\lambda x. x \ x)

前回の疑問への答え

  •  (\lambda x. x \ x)を型付けする(この項の型を一つ求める)だけなら全称型で十分(交差型でもOK)
    • たぶん、この項の使われ方に応じて適切に型付けすることもできる
  •  (\lambda x. x \ x)の主要型を求めたいなら、全称型だけでは不十分、交差型が必要

System Fでは、 (\lambda x. x \ x)を完全に多相的に受け取る関数、というかなり単純な例でも型付けできないということが分かりました。非常に強力な体系と言いつつ、意外と簡単に型付けできない項の例が作れるのですね。

*1:HaskellのrunSTがこれに該当し、特殊扱い(標準を逸脱した機能で実装)されているらしい?