型推論の規則

総称ラムダとかを参考にすると、次のようになる。ただし、これは厳密結合の推論で、型制約が出てこない。残念ながら、これでは実用にならないが、キレイにまとまる感じはある。

S, Tなどは型項（または型表現）、f, gなどはコマンド項、M, Nなどは式（formula）だとする。構文の定義は：

1. 名前はコマンド項である。
2. f, gがコマンド項なら、f|g もコマンド項である。（これで定義オシマイ）
3. S, Tが型項なら、S->T はプロファイルである。
4. αがプロファイル、tが型変数のとき、(t).α はプロファイルである。α内のtは束縛される。
5. fがコマンド項、αがプロファイルのとき、f:α は式である。
6. Mが式でtが型変数のとき、(t).M は式である。
7. Mが式、Sが型項のとき、M[S] は式である。

型項S, プロファイルα≡S->T に対して、置換作用 [U/t] が定義できる。[U/t]は、自由な型変数tを型項Uで置き換えること。型のベータ変換は以下のとおり。

• M≡f:S->T として、M[U/t] = f:S[U/t]->T[U/t]
• ((t).M)[U] ⇒ M[U/t]

以上の準備のもとで、次の推論規則が意味を持つ。Γは、型環境で、スキーマに対応する。

   Γ(f) = α のとき

  ------------------[base]

       f:α

 

   M:S->T  N:T->U

  ----------------[comp]

   M|N :S->U
   M:α （tは自由型変数）

  ----------------------[tabs]

    (t).M : (t).α
   M : (t).α

  -----------------[tapp]

   M[U] : α[U/t]

M:S->T N:T->U という前提を M:S->T N:U->V T⊆U にするのが安全結合。M:S->T N:U->V で、安全になるための再弱条件を求めるのが非安全結合。非安全結合の推論がやりたいこと。