Authors: Downen, Paul
Ariola, Zena
Ghilezan, Silvia 
Title: The Duality of Classical Intersection and Union Types
Journal: Fundamenta Informaticae
Volume: 170
Issue: 1-3
First page: 39
Last page: 92
Issue Date: 1-Jan-2019
Rank: M22
ISSN: 0169-2968
DOI: 10.3233/FI-2019-1855
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: discipline | duality | Intersection types | reducibility candidates | sequent calculus | soundness and completeness | strong normalization | symmetric candidates | type safety | union types
Publisher: IOS Press
Project: National Science Foundation, Grants CCF-1423617 and CCF-1719158
Representations of logical structures and formal languages and their application in computing 
Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education 

Show full item record


checked on Mar 20, 2023

Page view(s)

checked on Mar 21, 2023

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.