Type erasure
In programming languages, type erasure is the process of translating a program from a representation containing type information to one in which some or all of that information is omitted.[1] 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.[2]
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
- ↑ Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. pp. 109–110. ISBN 978-0-262-16209-8.
- ↑ Langer, Angelika. "What is reification?". https://www.angelikalanger.com/GenericsFAQ/FAQSections/TechnicalDetails.html#FAQ101A.
- Crary, Karl (2002). "Intensional Polymorphism in Type-Erasure Semantics". Journal of Functional Programming 12 (6): 567–600. doi:10.1017/S0956796801004282.
