In
programming languages
A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language.
The description of a programming ...
, type erasure is the
load-time
In computer systems a loader is the part of an operating system that is responsible for loading programs and libraries. It is one of the essential stages in the process of starting a program, as it places programs into memory and prepares them f ...
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 execu ...
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.
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 bicondi ...
it is the erasure of a well-typed explicitly typed
lambda term
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
), it does not always lead to an algorithm to check implicitly typed terms.
See also
*
Template (C++)
Template may refer to:
Tools
* Die (manufacturing), used to cut or shape material
* Mold, in a molding process
* Stencil, a pattern or overlay used in graphic arts (drawing, painting, etc.) and sewing to replicate letters, shapes or designs
Co ...
*
Problems with type erasure (in
Generics in Java
Generics are a facility of generic programming that were added to the Java programming language in 2004 within version J2SE 5.0. They were designed to extend Java's type system to allow "a type or method to operate on objects of various types whil ...
)
*
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