2004/03/23 by Matthew Fluet, Fluet, Matthew, Riccardo Pucella +1
Computer Science · #D.1.1 #D.3.3 #F.3.3 #FOS: Computer and information sciences #Logic, programming, and type systems #Natural Language Processing Techniques #Programming Languages (cs.PL) #Software Engineering Research #cs.PL
paper · pdf · doi:10.48550/arxiv.cs/0403034
41 pages. Preliminary version appears in the Proceedings of the 2nd IFIP International Conference on Theoretical Computer Science, pp. 448--460, 2002
openalex publication_date 2004/03/23 · arxiv created 2006/01/29 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.