# What are the relation and differences between reification and type passing semantics?

type erasure refers to the load-time process by which explicit type annotations are removed from a program, before it is executed at run-time. Operational semantics 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, the opposite of type erasure is called reification.

• Are both reification and type passing semantics opposite to type erasure?
• What are the relation and differences between reification and type passing semantics? Do they mean the same?

The best that I can find about them are from the two following books. But I am still not quite sure about my question.

About type erasure vs type passing, Types and Programming Languages by Pierce says:

23.7 Erasure and Evaluation Order

The operational semantics given to System F in Figure 23-1 is a type-passing semantics: when a polymorphic function meets a type argument, the type is actually substituted into the body of the function. The ML implementation of System F in Chapter 25 does exactly this. In a more realistic interpreter or compiler for a programming language based on System F, this manipulation of types at run time could impose a signiﬁcant cost. Moreover, it is easy to see that type annotations play no signiﬁcant role at run time, in the sense that no run-time decisions are made on the basis of types: we can take a well-typed program, rewrite its type annotations in an arbitrary way, and obtain a program that behaves just the same.

For these reasons, many polymorphic languages instead adopt a type-erasure semantics, where, after the typechecking phase, all the types are erased and the resulting untyped terms are interpreted or compiled to machine code.

About type erasure vs reification, Programming Language Pragmatics by Scott says:

C# 2.0 was able to employ an implementation based on reiﬁcation rather than erasure. Reiﬁcation creates a different concrete type every time a generic is instantiated with different arguments. Reiﬁed types are visible to the reﬂection library (csNames.GetType().ToString() returns "Arbiter 1[System.Double]"), and it is perfectly acceptable to call new T() if T is a type parameter with a zero-argument constructor (a constraint to this effect is required). Moreover where the Java compiler must generate implicit type casts to satisfy the requirements of the virtual machine (which knows nothing of generics) and to ensure type-safe interaction with legacy code (which might pass a parameter or return a result of an inappropriate type), the C# compiler can be sure that such checks will never be needed, and can therefore leave them out. The result is faster code.

Thanks.