Phantom Types and Subtyping

TL;DR

This paper explores the phantom-types technique, which uses parametric polymorphism and type constraints to model subtyping hierarchies in Hindley-Milner type systems like Standard ML, enabling encoding of complex hierarchies.

Contribution

It formally demonstrates how phantom-types can encode any finite subtyping hierarchy within Hindley-Milner type systems, including multiple inheritance structures.

Findings

Phantom-types can encode arbitrary finite subtyping hierarchies.

The technique is applicable to Hindley-Milner type systems like SML.

A formal translation from bounded polymorphism calculus to SML's type system is provided.

Abstract

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.