The Duality of Classical Intersection and Union Types

Issue title: Types, terms and reductions: A special issue dedicated to Paweł Urzyczyn for his 65th birthday

Guest editors: Thorsten Altenkirch and Aleksy Schubert

Article type: Research Article

Authors: Downen, Paul^{a; *} | Ariola, Zena M.^{a; *; †} | Ghilezan, Silvia^{b; ‡}

Affiliations: [a] University of Oregon, USA. pdownen@cs.uoregon.edu, ariola@cs.uoregon.edu | [b] University of Novi Sad, Mathematical Institute SASA, Republic of Serbia. gsilvia@uns.ac.rs

Correspondence: [†] Address for correspondence: University of Oregon, 1585 East 13th Avenue Eugene, OR 97403, USA

Note: [*] This work is supported by the National Science Foundation under grants CCF-1423617 and CCF-1719158.

Note: [‡] Courtesy Research Associate in the Global Studies Institute, University of Oregon. This work has been partly supported by MESTD under the grants ON174026 and III44006.

Abstract: For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to intersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest—soundness, completeness, and type safety—we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems—one for call-by-value and one for call-by-name evaluation—which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe.

Keywords: Intersection types, union types, duality, sequent calculus, discipline, type safety, strong normalization, soundness and completeness, reducibility candidates, symmetric candidates

DOI: 10.3233/FI-2019-1855

Journal: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 39-92, 2019