型解析のアルゴリズム

「勝たす異論」じゃねーよ。

型推論とかいうとつっこまれそうだから、型解析にする。問題はパイプ結合だけ。

1. 型ユニフィケーションをして、SIL命題のセットを出力する
2. SIL命題セットを整理、計算（簡約）する。
3. SIL命題セットから代入を取り出して、再帰的に（伝搬的に）適用する。
4. 残ったSIL命題を、SILエンジンにかける。
5. SILエンジンの結果を構文木にマークする。

これだけじゃ、わかんねーだろうけど。備忘。

[追記]

型ユニフィケーション Unify(S, T) では、次のどれかを出力する。

1. (S, y) -- yは変数、Sは任意の型項
2. (x, T) -- xは変数、Tは任意の型項
3. (a, b) -- a, b はスカラー型（定数項）

これは、連立不等式系のようなものだと考えられる。項Tに含まれる変数をVar(T)とすると、

1. Var(S) にyは含まれない。
2. Var(T) にxは含まれない。

ので再帰的な不等式系にはならない。

次の方式で“集約”する。

• (S, y), (S', y) ⇒ (S∪S', y)
• (x, T), (x, T') ⇒ (x, T∩T')

S∪S'と T∩T' は簡約する。

• tags(S)∩tag(S') = φ なら (S | S') を作り、そうでないならそのまま残す。
• T&T' を簡約計算ができなくなるまで計算する。

[/追記]