Catyは、トラブルの原因になりそうなことは、事前になるべく取り除こうという方針で作っています。
データのバリデーションは当然の事として、ハイパーリンクがちゃんと繋がることを保証しよう（ハイパーバリデーション）とか、リクエスト処理の途中で失敗しても被害を抑えるためにトランザクションをしっかりやろうとか、テストが負担にならない環境を作ろうとか、文書と実装の乖離をなくすために、自動描画や自動文書化のメカニズムを入れようとか、そんなことです。
当然に、リクエスト処理が“正しく”行われることも、できるだけ実行前に保証したいわけです。とは言っても「正しさ」とは何であるかの定義は難しいし、仮に定義が出来てもそれを完璧に保証するのは困難です。せめて型安全性くらいは保証したい、というのが我々の希望です。
最近、僕が論理と型推論の記事を書き始めたり、Kuwataさんも型システムに関するノートを書いたりしているのは、Catyに型安全性の判定系を付けるための準備みたいなものです。
型安全性の判定系は、その作業の一環としていわゆる「型推論」も行います。スクリプトコードを解析して、型の観点（型に注目するだけ）からそのコードを実行していいかどうかを調べます。「どうすれば型安全性の判定ができるか」は随分と前から（だいたいは）分かっていました。そもそも、型推論機能は、Catyプロジェクトの一番最初から予定されていた機能です。
予定はしてても手が回らないという事情は常にあるのですが、それよりネックになっていたのは、一箇所どうしても分からない事があったことです。「型安全かどうか？」にYES/NOで答えられても、実行時にチェックすべき型が決まらないのです。解がないから決まらないのではなくて、妥当な解がイッパイあり過ぎてどれを選んでいいか分からない、という状況でした。
型安全性が静的に分かるなら実行時型チェックは不要ではないか？ と思うでしょ。原理的には不要なんです。が、型に関する演繹をするとき、公理に相当する型宣言、例えば、foo :: string -> integer; はプログラマやアプリケーション設計者の自己申告なんです。開発中は（あるいは運用中でも）、自己申告と演繹に基づいたい名目上の安全性と実際の挙動に食い違いがあるかもしれません。そこで、静的に型安全と判定されても実行時型チェクを併用します。実行時チェック以外でも、型変数の具体化がないと困る箇所があります。
そのような型の具体化が決まらない問題があったのですが、比較的最近、どうやらうまくいきそうな気がしてきました。コロンブスの卵というか、僕に思い込みがあったようです。実は、苦し紛れにやってみた強引な方法がマトモな結果を出すので「えーーっ、こんなんで良かったん？」という状態なんですけどね。
ともかく、アルゴリズムはだいたい出来ていたし、引っかかっていた点は解決したみたい（たぶん）なので、自己流じゃない標準的な用語と記法で書き下そうと思い始めたのが1月末で、調べてみたら「標準的な用語と記法」と呼べるものはないし、山のような同義語／類義語でウンザリした、と ←今ココ。
それはそうと、以前、Catyの処理をCatyScriptで書いたことがあります（「REPL方式のWeb処理」とそこからのリンク先）。型推論の一部である単一化（ユニフィケーション）は、今のCatyScriptで書けそうです。実用にはなりませんが、説明には好都合です。CatyScriptのちょっと不便（非力）な部分をKuwataさんが修正してくれたので、単一化を書いてみようと思っています。
[追記 date="翌日"] いろいろと制限付きかつ手抜きですが、単一化を書いてみました。
面倒な事は省いてやってないからだとも言えますが、割と簡単に書けましたね。[/追記]
