ATS は Applied Type System フレームワークを根源とする、 高度に表現力のある型システム備えたプログラミング言語です。 それはまた ATS という言語の名前にもなっています。 ATS の型システムを徐々に説明します。 おそらくこの本で最も突出していて興味深い部分でしょう。
一般には、型を分類された値の集合のように扱います。 けれども、私は型を意味の形として扱う方がより適切であることを見つけました。 式に型を割り振る形式的な規則があり、それは型付け規則と呼ばれています。 もし式に型 T を割り振ることができるとします。 するとその式は型 T で表現された静的な意味 (意味論) を持つと言えるのです。 一つの式には複数の異なる静的な意味論を割り振られる可能性があることに注意してください。 もし式に割り振り可能な型 T が唯一1つだけ存在するなら、その式は正しい型付けをされていることになります。
もし型 T を持つ式と名前とを繋ぐ束縛が存在するなら、 束縛が有効なスコープにおいてその名前は型 T であると見なされます。 言い方を代えると、その名前は対応する式の持つ静的な意味を取るということになります。
exp0 が型 T の式であるとしましょう。 つまり型 T が exp0 に型付け規則によって割り振られたとします。 exp0 を exp1 に評価できるなら、exp1 もまた型 T が割り振れることになります。 別の言い方をすると、静的な意味は評価の中で不変であると言えるわけです。 この特性はしばしば 型保存 (type preservation) と呼ばれます。 これは ATS の型システムにおける健全性の一部です。 この特性に基づくと、exp0 がいくつかのステップで評価されて値になるとしても、 私達は型 T の取りうる値をたやすく推察することができるのです。
exp0 が型 T の式であり、また exp0 は値ではないとします。 すると exp0 は1ステップで別の式である exp1 に評価することがいつでも可能です。 この特性はしばしば プログレス (progress) と呼ばれます。 そしてこれは ATS の型システムにおける健全性のもう一つの部分です。