これでいいだろう：型検査と制約解決
静的型検査のアルゴリズムは、2009年末から2010年はじめに（2010-01-05, 2010-01-11）だいたいは考えた。その手順を述べると：
- スクリプトコードからデータフローグラフを作る。（プログラムで実行するなら記号的な操作となる。）
- データフローグラフのワイヤー（パイプ）ごとに型の単一化（ユニフィケーション）をする。単一化は基本的にロビンソンのアルゴリズムだが、等式ではなくて不等式を扱う点が異なる。
- 単一化の結果として制約系＝連立不等式系が出力されるので、その連立不等式系の解を求める。
制約系＝連立不等式系を解く部分が問題だが、ホーン論理式の連言と含意を持つ論理系に関する問題として定式化できる。この論理系はSIL（Simple Inclusion Logic）と呼んでいた。
連立不等式系の解法は、論理系SILの充足可能性問題と充足例問題と解釈きる。ここまではいいのだが、実際にこの充足問題を解くのはかなりめんどくさい。完全に解けるものかどうかわからない（可解性が不明）。そこで次を満たすアルゴリズムでよいとする。
ここで、「連立不等式系の解」と言っているのは、型変数の具体化である。実行時チェック条件は次の3つの要素で特定される。
- パイプの位置（一意的にパイプを特定できる）
- データの部分（パート）を抽出するパス式
- 具体的な型（型変数なし）
実行時には：
- 特定されたパイプを通るデータはチェックする。
- パス式で抽出された部分が、指定された具体型であればOK。そうでなければ型エラーで致命的ランタイムエラー。
連立不等式系の解を求める部分を型制約の解決（リゾリューション）と呼ぶとすると、解決アルゴリズムには幅がある。極端な例としては、常に失敗して実行時チェック条件だけを出力するアルゴリズムもありだ。上に述べたものは、静的型検査のフレームワークなので、解決アルゴリズムはプラッガブルとなっている。
さて、最近になって解決アルゴリズムの一例を具体的に構成した。あまり精度が高いアルゴリズムじゃないが、実用上は十分だと思う。論理操作によるものではなくて、有向グラフ上の値（型が値）の計算を行う。
不等式系の一部を等式に置き換えて、ダイクストラのアルゴリズムで値の伝搬と集約を行う。こうして連立等式系（不等式系じゃない！）の解を求める。この解が他の残った条件を満たすかどうかをチェックする。静的チェックがうまくいかなかったら実行時チェック条件を出力する。
実行時チェック条件をもとのスクリプトコードのパイプに貼り付けていく。パイプごとにチェック条件（0個から複数個）が付いたスクリプトができるが、型検査コマンドをその場所に展開すればよい。型検査の結果として出力されるスクリプトをCatyScript+eと呼んでいて、次の点が普通のCatyScriptと違う。
- スクリプトコードの冒頭に、__eval-options 内部コマンドを置ける。__eval-options --auto-type-check=false にセットする。
- スクリプトコードの __eval-options の次の位置に、__schemataブロックを置ける。ローカルに型定義が書ける。
- 型検査が必要な場所に、__validate-path 内部コマンドが配置される。
CatyScript+eをインタプリタ実行もできる（できたほうがよい）が、__schemataブロックの処理が重いので、かえって遅くなる可能性がある。__schemataブロックは、事前にコンパイルしてアンビエントに格納すれば効率が出るだろう。
