Type erasure

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.

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 Rule of inference for this definition.

See also

• Template (C++)
• Problems with type erasure (in Generics in Java)
• Monomorphization
• Type polymorphism

References

• Crary, Karl (2002). "Intensional Polymorphism in Type-Erasure Semantics". Journal of Functional Programming 12 (6): 567–600. doi:10.1017/S0956796801004282.