|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||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:||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
checked on Mar 21, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.