Subtyping with union types, intersection types and recursive types

Abstract

Union, intersection and recursive types are type constructions which make it possible to formulate very precise types. However, because of type checking difficulties related to the simultaneous use of these constructions, they have only found little use in programming languages. One of the problems is subtyping. We show how the subtype decision problem may be solved by an encoding into regular tree expressions, and prove soundness and completeness with respect to the classical ideal model for types [MPS86]. As a part of the work we show how the structure of values may be described by trees, and how the metric space of ideals may be related to a metric space of sets of trees. The proof techniques applied here may be of independent interest.