Set-Theoretic Types for Polymorphic Variants

TL;DR

This paper introduces a set-theoretic formalization of polymorphic variants in OCaml, resulting in a more expressive, intuitive, and predictable type system that enhances the theory of semantic subtyping.

Contribution

It proposes a set-theoretic approach to polymorphic variants, improving expressiveness, type safety, and predictability over existing implementations.

Findings

More expressive type system that types more programs

Removal of pathological cases leading to more predictability

Proof of completeness for the type reconstruction algorithm

Abstract

Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system whose behaviour is in some cases unintuitive and/or unduly restrictive. In this work, we present an alternative formalization of poly-morphic variants, based on set-theoretic types and subtyping, that yields a cleaner and more streamlined system. Our formalization is more expressive than the current one (it types more programs while preserving type safety), it can internalize some meta-theoretic properties, and it removes some pathological cases of the current implementation resulting in a more intuitive and, thus, predictable type system. More generally, this work shows how to add full-fledged union types to functional languages of the ML family that usually rely on the Hindley-Milner type system. As an aside, our system also improves the theory of semantic subtyping, notably by proving completeness for the type reconstruction algorithm.