Type Erasure

From Handwiki

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.[1]

Type inference

Main page: 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 require an algorithm to check implicitly typed terms.

See also

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

References

  1. Langer, Angelika. "What is reification?". http://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. 




Retrieved from "https://handwiki.org/wiki/index.php?title=Type_erasure&oldid=2646948"

Categories: [Type theory]


Download as ZWI file | Last modified: 12/30/2023 20:53:41 | 7 views
☰ Source: https://handwiki.org/wiki/Type_erasure | License: CC BY-SA 3.0

ZWI signed:
  Encycloreader by the Knowledge Standards Foundation (KSF) ✓[what is this?]