The recursive union of some gradual types

Abstract

We study union types and recursive types in the setting of a gradually typed lambda calculus. Our goal is to obtain a foundational account for languages that enable recursively defined data structures to be passed between static and dynamically typed regions of a program. We discuss how traditional sum types are not appropriate for this purpose and instead study a form of “true” union in the tradition of soft typing (Cartwright and Fagan, 1991) and occurrence typing (Tobin-Hochstadt and Felleisen, 2008). Regarding recursive types, our formulation is based on the axiomatization of subtyping by Brand and Henglein (1998). This paper defines three artifacts. First, in the context of the simply typed lambda calculus, we define the semantics of our unions and integrate them with equi-recursive types. Second, we add a dynamic type * to obtain a gradually typed lambda calculus. Its semantics is defined by translation to the third artifact, a blame calculus (Wadler and Findler, 2009) extended with unions and equi-recursive types.