パラメトリック多相性

• 多相関数 $f(x:t)$ が型 $t$ のパラメータ $x$ を持つとすると， $t$ は異なる実型に対して instantiate することができる．
• 陽に示すパラメトリック多相では， 型を関数の引数として渡す($f<t>(x:t)$)．関数呼び出しは， $f<\hbox{\tt int}>(3)$， $f<\hbox{\tt string}>(\hbox{\tt ''three''})$ のように書く．
• 陰に示すパラメトリック多相言語の $f$ は，$f(x)$ の定義に対して $f(\hbox{\tt 3})$ や $f(\hbox{\tt ''three''})$ と呼び出す． 型変数 $t$ は指定しない．
• 陰に型付けされた言語をコンパイルする場合にも，中間表現とし て，(表 16.1 に示す) 陽に型付けされた言語を使うには意味がある．
• 陽に型付けされた中間言語の最大の利点の一つは，中間表現が 型付け可能である(7 章で示した Tree 言語はそうではなかった)ことで ある．
• これにより，各最適化フェーズの後に，コンパイルされたプログラム をデバックしないように，コンパイラをデバックするために!， 型チェッカを(再び)実行する．

信用，しかし検証

• 型付き中間表現は，部分的にコンパイルされた(最適化された)プログラム の安全性とセキュリティをチェックするために役立つ．
• これは Web アプレット にとって重要な機能となる．例えば，Java プ ログラムは，Java 仮想機械バイトコードという中間言語にコンパイルする．
• セミコンパイルしたプログラムは，バイトコードベリファイアによ り(まだ)型チェックすることができ，ユーザマシンへ転送される．
• バイトコードプログラムは，インタプリットすることもできるし， ネイティブマシンコードに変換することもできる．
• バイトコード(または，他の変換された中間表現)の型チェックは，以下 のことを保証する．「アプレットが，型システムを violate することによりセキュリティを破壊 (subvert) しないという保証」 を，アプレットユーザが破らないようにする．
• しかし，Java はパラメトリック多相ではない．この章では，多相プ ログラミング言語のための型付き中間言語を示す．
• 多相を実現するために，陽に型づけされた多相言語である Poly-Tiger と 陰に示した多相言語 ImplicitPoly-Tiger を示そう．両方共に 15 章で示し た 関数言語 Fun-Tiger を基にしている．
• 両言語のために陽に型付けされた抽象構文は，Poly-Tiger に似ている．