システムF

システム F (多態的ラムダ計算または二次ラムダ計算とも呼ばれる) は、単純型付きラムダ計算に型の普遍量化のメカニズムを導入した型付きラムダ計算です。システム F は、プログラミング言語におけるパラメトリック多態性を形式化し、 HaskellやMLなどの言語の理論的基礎を形成します。これは、論理学者Jean-Yves Girard (1972) とコンピュータ科学者John C. Reynoldsによって独立に発見されました。

単純に型付けされたラムダ計算では項にわたる変数とそれらの結合子がありますが、System Fではさらに型にわたる変数とそれらの結合子があります。例えば、恒等関数がA → Aの形式の任意の型を持つことができるという事実は、System Fでは判断として形式化されます。

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

ここで、は型変数です。大文字は伝統的に型レベルの関数を表すのに使用され、小文字は値レベルの関数に使用されます。(上付き文字は、境界xが 型であることを意味します。コロンの後の式は、その前のラムダ式の型です。) ${\displaystyle \alpha}$${\displaystyle \Lambda}$${\displaystyle \lambda}$${\displaystyle \alpha}$${\displaystyle \alpha}$

項書き換えシステムとして、System F は強く正規化します。しかし、 System F の型推論(明示的な型注釈なし) は決定不能です。Curry –Howard 同型性の下では、System F は全称量化のみを使用する第 2 階直観論理のフラグメントに対応します。System F は、依存型を持つものを含む、さらに表現力豊かな型付きラムダ計算とともに、ラムダ キューブの一部と見なすことができます。

ジラールによれば、システムFの「F」は偶然選ばれたものである。^[1]

System F の型付け規則は、単純に型付けされたラムダ計算の規則に次の規則を追加したものです。

ここでは型、は型変数、 はコンテキスト内でがバインドされていることを示します。最初のルールは適用に関するもので、2番目のルールは抽象化に関するものです。 ^{[2] [3]}${\displaystyle \sigma ,\tau }$${\displaystyle \alpha}$${\displaystyle \alpha ~{\text{type}}}$${\displaystyle \alpha}$

型は次のように定義されます: 、ここで は型変数です。つまり、は、入力として型 α と 2 つの型 α の式を受け取り、出力として型 α の式を生成するすべての関数の型です ( は右結合であると見なすことに注意してください)。 ${\displaystyle {\mathsf {ブール値}}}$${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$${\displaystyle \alpha}$${\displaystyle {\mathsf {ブール値}}}$${\displaystyle \to}$

ブール値 と の次の 2 つの定義が使用され、Church ブール値の定義が拡張されます。 ${\displaystyle \mathbf {T} }$${\displaystyle \mathbf {F} }$

${\displaystyle \mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x}$

${\displaystyle \mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y}$

(上記の 2 つの関数には、 2 つではなく3 つの引数が必要であることに注意してください。 後の 2 つはラムダ式である必要がありますが、最初の引数は型である必要があります。 この事実は、これらの式の型が であるという事実に反映されています。 α をバインドする全称量指定子は、ラムダ式自体の alpha をバインドする Λ に対応します。 また、 はの便利な省略形ですが、System F 自体のシンボルではなく、「メタシンボル」であることに注意してください。 同様に、とも、System F「アセンブリ」(Bourbaki の意味で) の便利な省略形である「メタシンボル」です。 そうでなければ、そのような関数に名前を付けることができる場合 (System F 内)、関数を匿名で定義できるラムダ表現装置や、その制限を回避する 固定小数点コンビネータ は不要になります。)${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$${\displaystyle {\mathsf {ブール値}}}$${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$${\displaystyle \mathbf {T} }$${\displaystyle \mathbf {F} }$

次に、これら 2 つの-項を使用して、いくつかの論理演算子 ( 型) を定義できます。 ${\displaystyle \lambda}$${\displaystyle {\mathsf {ブール値}}\rightarrow {\mathsf {ブール値}}\rightarrow {\mathsf {ブール値}}}$

${\displaystyle {\begin{aligned}\mathrm {AND} &=\lambda x^{\mathsf {ブール値}}\lambda y^{\mathsf {ブール値}}{.}x\,{\mathsf {ブール値} }\,y\,\mathbf {F} \\\mathrm {OR} &=\lambda x^{\mathsf {ブール値}}\lambda y^{\mathsf {ブール値}}{.}x\,{\mathsf {ブール値}}\,\mathbf {T} \,y\\\mathrm {NOT} &=\lambda x^{\mathsf {ブール値}}{.}x\,{\mathsf {ブール値}}\,\mathbf {F} \,\mathbf {T} \end{aligned}}}$

上記の定義では、は の型引数であり、 に与えられる他の 2 つのパラメータが型であることを指定することに注意してください。Church エンコーディングと同様に、生の 型の項を決定関数として使用できるため、IFTHENELSE関数は必要ありません。ただし、要求された場合は、次のようになります。 ${\displaystyle {\mathsf {ブール値}}}$${\displaystyle x}$${\displaystyle x}$${\displaystyle {\mathsf {ブール値}}}$${\displaystyle {\mathsf {ブール値}}}$

${\displaystyle \mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}$

で十分です。述語は、型の値を返す関数です。最も基本的な述語はISZEROで、引数がチャーチ数字0の場合にのみを返します。 ${\displaystyle {\mathsf {ブール値}}}$${\displaystyle \mathbf {T} }$

${\displaystyle \mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T} }$

System F では、 Martin-Löf の型理論に関連した自然な方法で再帰構造を埋め込むことができます。抽象構造 ( S ) はコンストラクタを使用して作成されます。これらは次のように型付けされた関数です。

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}$。

再帰性は、 S自体がいずれかの型内に現れるときに現れます。これらのコンストラクタがm 個ある場合、 Sの型を次のように定義できます。 ${\displaystyle K_{i}}$

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }$

例えば、自然数はコンストラクタを持つ 帰納的データ型Nとして定義できる。

${\displaystyle {\begin{aligned}{\mathit {zero}}&:\mathrm {N} \\{\mathit {succ}}&:\mathrm {N} \rightarrow \mathrm {N} \end{aligned}}}$

この構造に対応するシステム F 型は です 。この型の項は、チャーチ数字の型付けされたバージョンで構成されており、最初のいくつかは次のとおりです。 ${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$

${\displaystyle {\begin{aligned}0&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x\\1&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx\\2&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)\\3&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))\end{aligned}}}$

カリー化された引数の順序を逆にすると（つまり）、 nのチャーチ数値は、関数f を引数として受け取り、fのn^乗を返す関数になります。つまり、チャーチ数値は高階関数であり、単一引数関数fを受け取り、別の単一引数関数を返します。 ${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }$

この記事で使用されている System F のバージョンは、明示的に型付けされた、または Church スタイルの計算です。λ 項に含まれる型付け情報により、型チェックが簡単になります。Joe Wells (1994) は、明示的な型付け注釈がない Curry スタイルの System F のバリアントでは型チェックが決定できないことを証明することで、「厄介な未解決問題」を解決しました。 ^{[4] [5]}

ウェルズの結果は、System F の型推論が不可能であることを示唆している。System F の制約である「 Hindley–Milner」、または単に「HM」には簡単な型推論アルゴリズムがあり、Haskell 98やMLファミリーなどの多くの静的型付け関数 型プログラミング言語で使用されている。時間の経過とともに、HM スタイルの型システムの制約が明らかになるにつれて、言語は着実に型システムのより表現力豊かなロジックに移行してきた。HaskellコンパイラーのGHC はHM を超えており (2008 年現在)、非構文型の等価性で拡張された System F を使用している。^[6] OCamlの型システムにおける HM 以外の機能にはGADTがある。^{[7] [8]}

第二階直観主義論理において、第二階多態的ラムダ計算 (F2) はジラール (1972) によって発見され、独立にレイノルズ (1974) によっても発見された。^[9] ジラールは表現定理を証明した。すなわち、第二階直観主義述語論理 (P2) において、自然数から自然数への全であることが証明できる関数は、P2 から F2 への射影を形成するということである。^{[9]レイノルズは}抽象定理を証明した。すなわち、F2 のすべての項は論理関係を満たし、その論理関係は P2 の論理関係に埋め込むことができるということである。^[9]レイノルズは、ジラール射影にレイノルズ埋め込みが恒等式、すなわちジラール-レイノルズ同型性を形成することを証明した。^[9]

システム F はBarendregt の ラムダ キューブの最初の軸に対応しますが、システム F _ωまたは高階多態的ラムダ計算は最初の軸 (多態性) と 2 番目の軸 (型演算子) を組み合わせた、より複雑な異なるシステムです。

システム F _{ω は}システムの族に対して帰納的に定義することができ、帰納は各システムで許可される 種類に基づいています。

• ${\displaystyle F_{n}}$許可の種類:
  • ${\displaystyle \star }$（種類）と
  • ${\displaystyle J\Rightarrow K}$ここで、および（引数の型が低次の型である、型から型への関数の種類）${\displaystyle J\in F_{n-1}}$${\displaystyle K\in F_{n}}$

極限では、システムを次のように 定義できる。${\displaystyle F_{\omega }}$

• ${\displaystyle F_{\omega }={\underset {1\leq i}{\bigcup }}F_{i}}$

つまり、F _ωは、引数 (および結果) が任意の順序になる可能性のある型から型への関数を許可するシステムです。

F _{ω は}これらのマッピングにおける引数の順序に制限を設けませんが、これらのマッピングの引数の範囲は制限します。つまり、引数は値ではなく型である必要があります。システム F _{ω は、値から型へのマッピング (}依存型)を許可しませんが、値から値へのマッピング (抽象化)、型から値へのマッピング (抽象化)、型から型へのマッピング (型レベルでの抽象化) は許可します。 ${\displaystyle \lambda }$${\displaystyle \Lambda }$${\displaystyle \lambda }$

システム F _{<: は}、「F-sub」と発音され、サブタイプ化を備えたシステム F の拡張です。システム F _{<: は、} 1980 年代からプログラミング言語理論において中心的な位置を占めてきました^{[要出典]。これは、} MLファミリーのような関数型プログラミング言語の中核が、システム F _<:で表現できるパラメトリック多態性とレコードサブタイプ化の両方をサポートしているためです。^{[10] [11]}

• 存在型​​— 普遍型の存在的に定量化された対応物
• システムU
• ラムダキューブ

• ピアス、ベンジャミン (2002)。「V ポリモーフィズム 第 23 章 ユニバーサルタイプ、第 25 章 システム F の ML 実装」。型とプログラミング言語。MIT プレス。pp.  339– 362、381– 388。ISBN 0-262-16209-1。

WikibooksにはHaskellに関する本があります。

• Franck Binard による System F の要約。
• System Fω: 現代のコンパイラの主力製品、Greg Morrisett著