「ソフトウェアの意味論は何のため／誰のために必要か」において、意味論（モデル）は精神衛生上の理由で必要だ、みたいなことを書きました。そればっかり強調すると、また変に誤解されかねないので、技術的／実用的な観点からの意味論の必要性についても敷衍＜ふえん＞しておきます。
意味論と対＜つい＞になる言葉は構文論です。構文の議論をちゃんとやろうとすると、意味論が必要です。以下、Catyについて話しますが、Catyでは型システムの役割が大きいので、型システムの構文論／意味論を話題とします。
内容：
型チェックがなぜ必要か
Catyでは、到るところで型チェックを行います。「どうして型チェックをするのか」というと、まず第一の理由は、人間の間違い（ミス）とそれに起因するトラブルを少なくするためです。間違いを少なくするためには、「間違いは必ず、しかもイッパイ発生する」という前提から出発します。「注意深くしよう」なんてお題目・説教はサッパリ役に立ちません。ともかく人間は常に間違うのですから。それと第二に、無謀なユーザーや悪意ある外部データから、Catyシステムとその配下のWebサイトを守るためにも型チェックが有効です。
無意識なあるいは故意の間違いがあっても、その間違いをソフトウェアが検出できること、間違いを残したまま実行されても被害を少なく抑えられることが重要です。この目的に対して、型チェックはコスト効率（設計・実装の負担に対する効果の比率）が最も高い手段です。
型の整合性を持たないコード（コマンドやスクリプト）が実行されれば、悪影響があるのは明かです。よって、そのようなコードの実行を食い止めるのが型チェックです。まずいコードがシステムに組み入れられる前に排除できれば理想的です。最悪でも、実行の最中に問題を検知して実行を中断することが必要です。実行中断は痛みを伴いますが、予測不可能な悪さをされるよりはマシです。
型推論と静的な型チェック
チェックというものは、なにかの基準がないと出来ません。型チェックの基準となるのは型宣言です。この型宣言というものは、プログラマには負担になります。そこで、最小限の型宣言だけを書いてもらい、派生的な型宣言はソフトウェアが計算により導出するのが望ましいでしょう。これが型推論機能です。
今のCatyプロトタイプには、型推論機能が実装されていませんが、アルゴリズムの目処はついています。この型推論アルゴリズムを使って、静的な型チェックを行う予定です。「静的」とは、実行をまったくせずに型の整合性を判断するということです。
ただし、静的な型チェックは完璧にはできません。むしろ、実行時型チェックをはずせる場所を探すことが静的型チェックだと思ったほうがいいでしょう。それに、当初は静的型チェッカー・プログラムのバグの懸念もあるので、静的型チェックと実行時型チェックの二重の検査をすることは意味があります。
静的型チェッカーが十分信頼できる水準になれば、静的に安全だと保証された部分では実行時チェックをはずせば、パフォーマンス向上に役立ちます。
型宣言を書く動機付け
型推論機能があっても、一番根本のところ、ネイティブコマンド（Pythonで書かれたコマンド）にはプログラマによる型宣言が必要です。この型宣言は自己申告です。ここで嘘や曖昧な情報が入力されると、型システムは破綻します。是非にちゃんと宣言を書いて欲しい。でも、型宣言を書く行為は面倒なので、作法やモラルだけでなく、それなりの見返りが必要な気がします。
まず、当然ですが、正しい型宣言（コマンド宣言）を書けば、入出力の型チェックコードをコマンド側で書く必要がほぼ無くなります。「ほぼ」と書いたのは、スキーマでは表現不可能な制約があれば、それはプログラムコードとして書くしかないからです（そういうケースは稀だと思いますが）。
Catyの型宣言では、データの入出力だけでなく、使用するストレージ（メモリ、ディスクファイル、データベース、外部Webサービスなど）や発生するかもしれない例外も書きます。ストレージの使用宣言をしないと、そのストレージは使えません。これは、インセンティブじゃなくてペナルティみたいですが、宣言をしていれば、トランザクションやセキュリティの面倒はすべてシェル（Caty実行環境）がみてくれるのでラクチンなのです。
そんな事情で、型宣言には十分な見返りがあると思います。
型推論演繹系と意味論
今説明したように、型推論機能を持った型システムがCatyの重要な構成要素となるのですが、そのアルゴリズムや実装が正しいことはどうやって保証や確認ができるでしょうか？ 僕（檜山）が「私達を信じてください」とか言っても意味ないですよね。第一、僕自身が自分のこと信用してないですから。
そこで登場するのが意味論（モデル）です。コードという構文的対象（所詮は記号列）に対して、それが指し示す構造物とか実行とかが何であるかを抽象的に定式化したものが意味論です。ソースコードと同様に、構文論と意味論を公開しておけば、ミスや変なところがあれば、誰でもそれを指摘できます。第三者が評価可能なほどに明白に構文論／意味論を記述するのは相当に大変なのですが、「できるだけやってみるわ」とは言っておきます。
Catyの場合は、「スクリプトコードが指し示すモノが存在する」ことと、「ある論理式が証明可能である」ことと、「コードの実行がうまくいく」ことが同値になります； スクリプトコードEがあると、それに対応する論理式Qが作れます。QはEに依存するので Q(E) と書いたほうが正確ですが、面倒なので単にQとも記します。論理式Qが、とある演繹系で証明可能なことを |- Q と書きます。意味論的にQが正しいことを |= Q と書きます。次の事実が基本的です。
- |= Q ならば、Eの実行がうまくいく
- Eの実行がうまくいくならば、|= Q
ここで、「うまくいく」という言葉が曖昧ですが、「破綻せずに期待した結果が得られる」（これも曖昧だ）くらいに思ってください。注意すべきは、「うまくいく」が例外を出さないという意味ではないことです。例外が発生可能であると予測されていて、実際に例外が出ることは「うまくいく」の範囲内です。
ともかく、|= Q （意味論的にQが正しい）は、「Eの実行がうまくいく」と同義です。当該の演繹系（それは型推論の演繹系です）が健全（sound）ならば、次が成立します。
- |- Q ならば、|= Q
つまり、実行前に型推論でOKがでれば、実行がうまくいくことが保証されます。いやー、素晴らしい -- ところが、そうは問屋が卸さないのです。
実行時チェックを併用するわけ
できるだけ扱いやすい簡単な型システムを作ってみても、次の性質を持たせるのは至難のワザです。
- 任意のスクリプトコードEに対して、Q = Q(E) が証明可能か、または、Qの否定が証明可能である。
実用上の要求から、Catyは型変数（総称型）を持つので、任意の論理式Qの真偽が決定可能にはなりません。しかし、Qに対して次の性質を持つ論理式Pを実効的に探すことができます。
- P⊃Q が証明可能である。
ここで、記号「⊃」は含意です。このPが「なんでもいい」なら、Q自身を選んで「Q⊃Q は証明可能」とできるのでナンセンスです。「なんでもいい」のではなくて：
- X⊃Q が証明可能となるXのなかで最も弱い条件であるP
つまり、Qであることを保証するギリギリ、最低限の条件がPです。そういうPを見つけることはできるのですが、Pが実際に成立しているかどうかはサッパリわかりません。Pの成立／不成立は事実と付き合わせて確認するしかないのです。言い換えれば、Pのチェックは実行時にしかできません。
型推論の演繹系が健全であれば、
- |- (P⊃Q) ならば、|= (P⊃Q)
です。そして、|= (P⊃Q) は次の形に言い換えることができます。
|= P ならば、|= Q
任意のモデルxに対して、x |= P ならば、x |= Q （[追記]訂正しました[/追記]）
条件Pは、実行時の検査項目です。x |= Q は「（実行時状態xのもとで）Eの実行がうまくいく」ことだったので、
- 条件Pが実行時に成立するならば、Eの実行がうまくいく
となります。前述のごとく、Pは事前に求められるので、実行時にチェックすべき最小限の項目を、実行前に（静的に）推論により確定できることになります。
静的チェックと実行時チェックを併用することになりますが、実行時チェックを完全に落とすのは難しいので、ここらへんで妥協しようと思っています。
