#型システム[*** 問題]非純粋･call by value･多相の3つが揃うとき大変なことが起こる｡今､value restrictionのないML方言と参照セルとリストコンストラクタを用意する｡let多相があると､let-boundなものを多相にすることができる｡`r`は多相なリスト`'a list`を持っているので`'a list ref` 型になる｡さて､`r`のリストの参照を更新していくわけだが

[**** [$ \left(\lambda x. x\right) \left(\lambda x. x\right) ]]ラムダ抽象と適用から成る､非常に単純でありながら[チューリング完全]である計算体系｡現在多くのプログラム言語に備わっている第一級関数(無名関数､クロージャ､etc.)はラムダ計算に基づいている(場合があるぞい)｡型なし[型なしラムダ計算] (untyped lambda calculus)

#ラムダ計算[- 力なり]残りの計算を指す｡[** 基本] 継続は動的に現れ､あらゆる位置に存在する｡

#型システム型を受け取って型を返す型 (`* → *`)｡高階型､Higher Rank Typesとも｡HKTと略される｡例えばHKTの無い[OCaml]では､`'a list` は[* 型ではなく型コンストラクタ]という扱いになっているが､HKTのある[Haskell](`List A` または `[A]`)では `* → *` という `A`型を受け取って`[A]`を返す[* 型]である｡式を取って式を返すという関数が式であるとさまざまな実りがある(c.f. [ラムダ計算])ように､型を受け取って型を返すという仕組みも型に含まれているとさまざまな嬉しさがある｡

#ラムダ計算`let`を除くすべての項が副項を持たないように書いていく方式｡特に関数型言語向けコンパイラの中間言語として､[CPS (continuation-passing style, 継続渡し方式)]と並ぶ存在｡ANFは[チューリング完全]だったとおもう副項を持たないようにするために､`let`式を用いて副項になる部分を変数に束縛していく｡この点から[SSA]と非常に類似している｡[** 基本例]

#ラムダ計算すべての[継続]を明示的に書いていく方式｡特に関数型言語向けコンパイラの中間言語として､[A-Normal Form]と並ぶ存在｡CPSは[チューリング完全]だったとおもう継続はコントロールフローとして見ることもでき､CPSへの変換によってfor文やearly return､例外なども表現できる｡[** 基本例]

#型システム #ラムダ計算[* 二階ラムダ計算] や [* 多相ラムダ計算] として知られる｡またこれを型システムに埋め込むことで強力な型を表現できる｡簡単な例として､よくある `id` 関数をSystem Fで表すとこのようになる｡[$ \mathit{id} = \Lambda a. \lambda x : a. x \rightarrow x][$ x]の[* 型を[$ a]でパラメタライズ] することで[* 多相性] を獲得している｡