型チェックと型推論 - 檜山正幸のキマイラ飼育記 (はてなBlog)「ソフトウェアの意味論は何のため／誰のために必要か」において、意味論（モデル）は精神衛生上の理由で必要だ、みたいなことを書きました。そればっかり強調すると、また変に誤解されかねないので、技術的／実用的な観点からの意味論の必要性についても敷衍＜ふえん＞しておきます。 意味論と対＜つい＞になる言葉は構文論です。構文の議論をちゃんとやろうとすると、意味論が必要です。以下、Catyについて話しますが、Catyでは型システムの役割が大きいので、型システムの構文論／意味論を話題とします。 内容： 型チェックがなぜ必要か 型推論と静的な型チェック 型宣言を書く動機付け 型推論演繹系と意味論 実行時チェックを併用するわけ 型チェックがなぜ必要か Catyでは、到るところで型チェックを行います。「どうして型チェックをするのか」というと、まず第一の理由は、人間の間違い（ミス）とそれに起因するトラブルを少なくす
