型消去

プログラミング言語において、型消去とは、実行時にプログラムが実行される前に、明示的な型注釈をプログラムから削除するロード時のプロセスです。 プログラムに型が付随することを必要としない操作的意味論は、型渡し意味論とは対照的に、型消去意味論と呼ばれます。型消去意味論は抽象化原理であり、プログラムの実行時の実行が型情報に依存しないことを保証します。ジェネリックプログラミングの文脈では、型消去の反対は具体化と呼ばれます。^[1]

逆の操作は型推論と呼ばれます。型の消去は暗黙的に型付けされた言語で型付けを定義する簡単な方法ですが (暗黙的に型付けされた項は、適切に型付けされた明示的に型付けされたラムダ項の消去である場合にのみ、適切に型付けされます)、この定義の 推論規則は提供されません。

• テンプレート (C++)
• 型消去の問題( Java のジェネリック)
• 単形化
• 型多態性

• Crary, Karl; Weirich, Stephanie ; Morrisett, Greg (2002). 「型消去セマンティクスにおける内包的多態性」. Journal of Functional Programming . 12 (6): 567–600. CiteSeerX  10.1.1.5.4507 . doi :10.1017/S0956796801004282.