In
programming languages
A programming language is a system of notation for writing computer program, computer programs. Most programming languages are text-based formal languages, but they may also be visual programming language, graphical. They are a kind of computer ...
, 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
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execut ...
that do not require programs to be accompanied by types are called ''type-erasure semantics'', to be contrasted with ''type-passing semantics''. The possibility of giving type-erasure semantics is a kind of
abstraction principle, ensuring that the run-time execution of a program does not depend on type information. In the context of
generic programming
Generic programming is a style of computer programming in which algorithms are written in terms of types ''to-be-specified-later'' that are then ''instantiated'' when needed for specific types provided as parameters. This approach, pioneered b ...
, the opposite of type erasure is called
reification
Reification may refer to:
Science and technology
* Reification (computer science), the creation of a data model
* Reification (knowledge representation), the representation of facts and/or assertions
* Reification (statistics), the use of an id ...
.
Type inference
The reverse operation is called
type inference
Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistics. ...
. 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
In logic and related fields such as mathematics and philosophy, "if and only if" (shortened as "iff") is a biconditional logical connective between statements, where either both statements are true or both are false.
The connective is bi ...
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.
See also
*
Template (C++)
*
Problems with type erasure (in
Generics in Java)
*
Type polymorphism
In programming language theory and type theory, polymorphism is the provision of a single interface to entities of different types or the use of a single symbol to represent multiple different types.: "Polymorphic types are types whose operatio ...
References
*
Type theory
{{comp-sci-stub