Phantom Types and Subtyping

Title: Phantom Types and Subtyping

Research Question: How can we use phantom types and subtyping to create a safe programming environment?

Methodology: The researchers proposed a technique called the "phantom-types technique." This technique uses parametric polymorphism, type constraints, and unification of polymorphic types to model a subtyping hierarchy. They demonstrated this technique's suitability for capturing first-order subtyping by exhibiting a type-preserving translation from a simple calculus with bounded polymorphism to a calculus embodying the type system of Standard ML (SML).

Results: The researchers showed that the phantom-types technique can be used to encode any finite subtyping hierarchy, including hierarchies arising from multiple interface inheritance. They also provided an example using SML to illustrate how the technique can be used to create a safe programming environment.

Implications: The phantom-types technique provides a way to use the SML type system to capture subtyping hierarchies and create a safe programming environment. This can lead to more robust and reliable software, as it allows for the detection of type errors at compile time rather than run time. The technique's ability to work with any finite subtyping hierarchy makes it applicable to a wide range of programming scenarios.

Link to Article: https://arxiv.org/abs/0403034v3 Authors: arXiv ID: 0403034v3