{{Short description|Process by which explicit type annotations are removed from a program}} In programming languages, '''type erasure''' is the load-time process by which explicit type annotations are removed from a program, before it is executed at run-time. Operational semantics not requiring programs to be accompanied by types are named ''type-erasure semantics'', in contrast with ''type-passing semantics''. Type-erasure semantics is an abstraction principle, ensuring that the run-time execution of a program doesn't depend on type information. In the context of generic programming, the opposite of type erasure is named reification.<ref>{{cite web|last1=Langer|first1=Angelika|title=What is reification?|url=https://www.angelikalanger.com/GenericsFAQ/FAQSections/TechnicalDetails.html#FAQ101A}}</ref>
== Type inference == {{Main|Type inference}} The reverse operation is named type inference. Though type erasure can be 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 doesn't provide rules of inference for this definition.
==See also== * Template (C++) * Problems with type erasure (in Generics in Java) * Monomorphization * Type polymorphism
==References== {{Reflist}} * {{cite journal | first1 = Karl | last1 = Crary | first2 = Stephanie | last2 = Weirich | author2-link= Stephanie Weirich | first3 = Greg | last3 = Morrisett | title = Intensional Polymorphism in Type-Erasure Semantics | journal = Journal of Functional Programming | volume = 12 | issue = 6 | pages = 567–600 |doi = 10.1017/S0956796801004282 | year = 2002 | citeseerx = 10.1.1.5.4507 }}
Category:Type theory
{{comp-sci-stub}}