与えられた項（term）に型付け（typing）することは、型に関わる基本的行為ですが、なにかしら項の書き方（構文）を決めておかないと例を出せません。普通はラムダ項が使われるのですが、もっと馴染みがある構文を定義しておきましょう。以下で、項（term）と式（expression）は同じ意味で使います（使い分けの基準はありません）。
内容：
- ラムダ項をJavaScript風に書く
- let式
- 型let式
シリーズ目次：
ラムダ項をJavaScript風に書く
ラムダ計算の説明にJavaScriptは好都合です（「JavaScriptで学ぶ・プログラマのためのラムダ計算」を参照）。λ(x, y).(x + y) を function (x, y){return (x + y);} と書けます。だけど、return がいかにも邪魔ですね（「returnも嫌いな理由」も参照）。returnは書かなくてもいいことにしましょう。つまり、function (x, y){x + y} でいい、と。これならもう、ほとんどラムダ項そのもの。
関数の引数と戻り値の型を次の形で宣言できるとします。
- function (x:integer, y:integer):integer {x + y}
これは型付きラムダ項に対応します。ただし、型宣言は必須ではなくて、あってもなくてもいいとします。
引数変数だけでなく、どこに出現した変数にも型を添えていいとします。例えば、
- function (x, y):integer {x:integer + y:integer}
出現位置のその場で型宣言をするようなものです。このような形での、変数への型情報付与を型注釈（type annotation）と言います。最初に出した、引数と戻り値の型宣言も型注釈とみなして差し支えありません。
let式
変数を束縛しておいてから式を評価することを表すためにlet式がよく使われます。次の形を使います。
- let ＜変数束縛＞ in ＜式＞
JavaScript風構文でもlet式を使っていいとします。
- let {var x=2; var y=3} in {x + y}
この例では、x + y は 2 + 3 となり、全体の値は5です。すべての変数が束縛される必要はありません。
- let {var x=2} in {x + y}
これだと、x + y が 2 + y になりますが、それ以上は評価できません。
- let {var y=3} in {function (x) {x + y}}
これは、function (x) {x + 3} が値となります。
- let {var x=2} in {(let {var y=3} in {function (x) {x + y}})(x)}
少し複雑ですが、注意深く順番に見ていけば、次と同じことがわかると思います。
- (function (x) {x + 3})(2)
次はどうでしょうか？ 考えてみてください。
- let {var x=2} in {let {var y=3} in {let {var f = function (x) {x + y}} in {f(x)}}}
型let式
let式は、変数に値を束縛します。値には関数も含まれます（let {var f = function (x) {x + y}} がその例）。式の評価のための環境を整えていることになります。一方、式の型を知りたいときは、型付け（typing）の環境が必要です。それは、変数や関数の戻り値に型注釈を付けることになります。
型注釈を付けるための専用の構文、例えば lettype {var x:integer; var t:boolean} を導入してもいいのですが、めんどうだからletをそのまま使ってしまいましょう。
- let {var x:integer; var t:boolean} in {function (y:integer) {if (t) {x} else {y}}}
function (y:integer) {if (t) {x} else {y}} だけだと、yの型しかわかりませんが、外側のletにおいて、x:integer; var t:boolean と型注釈（型宣言）されているので、x, y, tの型がハッキリとわかります。
let内では、変数の型注釈と値の束縛を一緒にやってもいいとします。
- let {var x:integer=2; var t:boolean} in {function (y:integer) {if (t) {x} else {y}}}
if (t) {x} else {y} のような式だけだと、変数の型も値も不明です。let式によって、型情報や値情報を準備してあげることができます。すべての情報を明示的に与えなくても、与えられた情報をもとに計算や推論ができます。できるだけ少ない型注釈から、式やその部分式の型を決定することが、「型推論」のひとつの解釈です。
