考えなおした結果

型解析系がやること：

1. プロファイルのないスクリプトを解析して、プロファイル（宣言）を作る。
2. 人間がプロファイルを書いているとき、そのプロファイルが正しいかどうかをチェック。
3. 実行時の安全性を保証する。

1,2番はそれほど重要じゃなくて、重要なのは3番目。

次のように記号を約束する。

1. E, F はスクリプト式
2. x, y などは型変数
3. S, T などは型変数を含むかもしれない型項
4. A, B などは閉じた（型変数を含まない）型項

式Eが与えられれば、パイプの位置をチェックして番号をつけることができる。nをパイプ番号とする。

式Eが整合的である条件をConsis(E)とすると、Consis(E)は次の形の制約（不等式）の集まりとなる。

• [n] S⊆T

これがパイプの数（入り口、出口を含めるかもしれない）だけの連立となる。

Cosis(E)の制約（連立不等式）を、型項の単一化で解くと、次の形のパス付き制約が出てくる。

1. [n] p : x⊆y
2. [n] p : x⊆B
3. [n] p : A⊆y

nはパイプ番号、pはパス。xのカインドをK、yのカインドをLとすると、これらの制約は次の実行時チェック条件になる。

1. [n] p : sup(K)∧sup(L)
2. [n] p : sup(K)∧B
3. [n] p : A∧sup(L)

これで「実行時の安全性は保証」できているハズ。総称プロファイルを持つコマンドの解釈を厳密化して、安全であることを証明すればいい。それが出来るなら、他の問題は気にするほどのことではないだろう。