Phantom Types and Subtyping

  • jfp06.pdf (with Riccardo Pucella; To appear in the Journal of Functional Programming)

    We investigate a technique from the literature, called the phantom-types technique, that uses parametric polymorphism, type constraints, and unification of polymorphic types to model a subtyping hierarchy. Hindley-Milner type systems, such as the one found in Standard ML, can be used to enforce the subtyping relation, at least for first-order values. We show that this technique can be used to encode any finite subtyping hierarchy (including hierarchies arising from multiple interface inheritance). We formally demonstrate the suitability of the phantom-types technique 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 SML.

  • arXiv04.pdf (with Riccardo Pucella; Unpublished; split into the JFP paper above and the practical datatype specializations paper)

    We investigate a technique from the literature, called the phantom types technique, that uses parametric polymorphism, type constraints, and unification of polymorphic types to model a subtyping hierarchy. Hindley-Milner type systems, such as the one found in SML, can be used to enforce the subtyping relation. We show that this technique can be used to encode any finite subtyping hierarchy (including hierarchies arising from multiple interface inheritance). We formally demonstrate the suitability of the phantom types technique for capturing subtyping by exhibiting a type-preserving translation from a simple calculus with bounded polymorphism to a calculus embodying the type system of SML. We then illustrate a particular use of the technique to capture programming invariants associated with user-defined datatypes, in the form of statically-enforced datatype specializations.

  • tcs02.ps (with Riccardo Pucella; Appeared at TCS'02; 20020829-TCS02.ppt)

    We investigate a technique from the literature, called the phantom types technique, that uses parametric polymorphism, type constraints, and unification of polymorphic types to model a subtyping hierarchy. Hindley-Milner type systems, such as the one found in ML, can be used to enforce the subtyping relation. We show that this technique can be used to encode any finite subtyping hierarchy (including hierarchies arising from multiple interface inheritance). We then formally demonstrate the suitability of the phantom types technique for capturing subtyping by exhibiting a type-preserving translation from a simple calculus with bounded polymorphism to a calculus embodying the type system of ML.


The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.