多相化ラムダ

http://ttic.uchicago.edu/~pl/classes/CMSC336-Winter08/lectures/lec10.pdf に、次の推論規則が載っていた。
「Xは型です」を X type と書くことにして、

 Δ, α type |- τ type

 ----------------------

      Δ |- ∀α.τ

 Δ, α type; Γ |- e : τ

 --------------------------

 Δ; Γ |- Λα.e : ∀α.τ

セミコロンの左が型コンテキストで、右が評価環境なのだと思う。型コンテキストだけの∀導入はわかりやすい。Λα.e : ∀α.τ は、型項と項の両方を同時に型変数で束縛する。∀α.τ はいわゆる多相型。Λα.e は多相項か？ 項eを型変数で多相化する操作がΛなのだろう。

この例では、値に関する関数抽象がλ、型に関する全称束縛がΛとなっている。型に関する全称束縛を、型項も値項も同じ∀を使っている例がある。

∀α.(e : τ) = (Λα.e : ∀α.τ) と考えればいいのかな？ それなら、∀α.(e : τ) = (∀α.e : ∀α.τ) が分かりやすいかも。