A gradual interpretation of union types

Abstract

Union types allow to capture the possibility of a term to be ofseveral possibly unrelated types. Traditional static approaches to uniontypes are untagged and tagged unions, which present dual advantagesin their use. Inspired by recent work on using abstract interpretation tounderstand gradual typing, we present a novel design for union types,called gradual union types. Gradual union types combine the advan-tages of tagged and untagged union types, backed by dynamic checks.Seen as a gradual typing discipline, gradual union types are restrictedimprecise types that denote a finite number of static types. We applythe Abstracting Gradual Typing (AGT) methodology of Garcia et al. toderive the static and dynamic semantics of a language that supports bothgradual unions and the traditional, totally-unknown type. We uncoverthat gradual unions interact with the unknown type in a way that man-dates a stratified approach to AGT, relying on a composition of twodistinct abstract interpretations in order to retain optimality. Thanks tothe abstract interpretation framework, the resulting language is type safeand satisfies the refined criteria for gradual languages. We also show howto compile such a language to a threesome cast calculus, and prove thatthe compilation preserves the semantics and properties of the language.