Jump to content

Type erasure

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Sae1962 (talk | contribs) at 15:28, 5 September 2012 (Added a link). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

In programming languages, type erasure refers to the compile-time process by which explicit type annotations are removed from a program, before it is executed at run-time. An operational semantics that does not require programs to be accompanied by types is called a type-erasure semantics, to be contrasted with a type-passing semantics. The possibility of giving a type-erasure semantics is a kind of abstraction principle, ensuring that the run-time execution of a program does not depend on type information.

Reverse operation

The reverse operation is called type inference. Though type erasure can be used as an easy way to define typing over implicitly typed languages (an implicitly typed term is well-typed if and only if it is the erasure of a well-typed explicitly typed lambda term), it does not always lead to an algorithm to check implicitly typed terms.

References

  • Crary, Karl; Weirich, Stephanie; Morrisett, Greg (2002). "Intensional Polymorphism in Type-Erasure Semantics". Journal of Functional Programming. 12 (6): 567–600. {{cite journal}}: Cite has empty unknown parameter: |booktitle= (help)

See also