article

Disjoint intersection types

Authors:

Bruno C. d. S. Oliveira,

João AlpuimAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 9

Pages 364 - 377

https://doi.org/10.1145/3022670.2951945

Published: 04 September 2016 Publication History

Abstract

Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression can elaborate to expressions that evaluate to different values. The lack of coherence is an important disadvantage for adoption of his core calculus in implementations of programming languages, as the semantics of the programming language becomes implementation-dependent.

This paper presents λ_i: a coherent and type-safe calculus with a form of intersection types and a merge operator. Coherence is achieved by ensuring that intersection types are disjoint and programs are sufficiently annotated to avoid type ambiguity. We propose a definition of disjointness where two types A and B are disjoint only if certain set of types are common supertypes of A and B. We investigate three different variants of λ_i, with three variants of disjointness. In the simplest variant, which does not allow ⊤ types, two types are disjoint if they do not share any common supertypes at all. The other two variants introduce ⊤ types and refine the notion of disjointness to allow two types to be disjoint when the only the set of common supertypes are top-like. The difference between the two variants with ⊤ types is on the definition of top-like types, which has an impact on which types are allowed on intersections. We present a type system that prevents intersection types that are not disjoint, as well as an algorithmic specifications to determine whether two types are disjoint for all three variants.

References

[1]

N. Amin, A. Moors, and M. Odersky. Dependent object types. In 19th International Workshop on Foundations of Object-Oriented Languages, 2012.

[2]

N. Amin, T. Rompf, and M. Odersky. Foundations of path-dependent types. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014.

Digital Library

[3]

B. E. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich. Engineering formal metatheory. In G. C. Necula and P. Wadler, editors, Proceeding of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 3–15. ACM, 2008.

Digital Library

[4]

V. Benzaken, G. Castagna, and A. Frisch. CDuce: An XML-centric general-purpose language. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP ’03, 2003.

Digital Library

[5]

L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988.

Digital Library

[6]

G. Castagna, G. Ghelli, and G. Longo. A calculus for overloaded functions with subtyping. In Proceedings of the 1992 ACM Conference on LISP and Functional Programming, LFP ’92, 1992.

Digital Library

[7]

G. Castagna, K. Nguyen, Z. Xu, H. Im, S. Lenglet, and L. Padovani. Polymorphic functions with set-theoretic types: Part 1: Syntax, semantics, and evaluation. In Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’14, 2014.

Digital Library

[8]

A. B. Compagnoni and B. C. Pierce. Higher-order intersection types and multiple inheritance. Mathematical Structures in Computer Science, 1996.

[9]

M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Mathematical Logic Quarterly, 27(2–6):45–58, 1981.

[10]

P.-L. Curienl and G. Ghelli. Coherence of subsumption. In CAAP’90: 15th Colloquium on Trees in Algebra and Programming, Copenhagen, Denmark, May 15-18, 1990, Proceedings, volume 431, page 132. Springer Science & Business Media, 1990.

Digital Library

[11]

R. Davies. Practical refinement-type checking. PhD thesis, Carnegie Mellon University, 2005.

Digital Library

[12]

R. Davies and F. Pfenning. Intersection types and computational effects. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP’00), 2000.

Digital Library

[13]

J. Dunfield. Refined typechecking with Stardust. In A. Stump and H. Xi, editors, Programming Languages meets Program Verification (PLPV ’07), Freiburg, Germany, Oct. 2007.

Digital Library

[14]

J. Dunfield. Elaborating intersection and union types. Journal of Functional Programming, 2014.

[15]

J. Dunfield and F. Pfenning. Type assignment for intersections and unions in call-by-value languages. In A. Gordon, editor, Foundations of Software Science and Computation Structures (FOSSACS ’03), pages 250–266, Warsaw, Poland, Apr. 2003. Springer-Verlag LNCS 2620.

Digital Library

[16]

J. Dunfield and F. Pfenning. Tridirectional typechecking. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’04, 2004.

Digital Library

[17]

T. Freeman and F. Pfenning. Refinement types for ML. In Proceedings of the SIGPLAN ’91 Symposium on Language Design and Implementation, Toronto, Ontario, June 1991. ACM Press.

Digital Library

[18]

M. P. Jones. Coherence for Qualified Types. Technical Report YALEU/DCS/RR-989, Yale University, 1993.

[19]

M. P. Jones. Qualified Types: Theory and Practice. Cambridge University Press, Cambridge, England, 1994.

Digital Library

[20]

M. Odersky et al. An overview of the Scala programming language. Technical Report IC/2004/64, EPFL Lausanne, Switzerland, 2004.

[21]

F. Pfenning and C. Schürmann. System description: Twelf — A metalogical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the International Conference on Automated Deduction, pages 202–206, 1999.

Digital Library

[22]

B. C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991.

[23]

B. C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, December 1991.

Digital Library

[24]

B. C. Pierce. Intersection types and bounded polymorphism. Mathematical Structures in Computer Science, 1997.

Digital Library

[25]

B. C. Pierce and D. N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1), Jan. 2000.

Digital Library

[26]

G. Pottinger. A type assignment for the strongly normalizable λ-terms. In To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pages 561–577. Academic Press, London, 1980.

[27]

J. C. Reynolds. The coherence of languages with intersection types. In Proceedings of the International Conference on Theoretical Aspects of Computer Software, TACS ’91, 1991.

Digital Library

[28]

J. C. Reynolds. Design of the Programming Language Forsythe, pages 173–233. Birkhäuser Boston, Boston, MA, 1997.

Digital Library

[29]

J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on, pages 55–74. IEEE, 2002.

Digital Library

[30]

S. van Bakel. Complete restrictions of the intersection type discipline. Theoretical Comput. Sci., 99, 1992.

Digital Library

[31]

P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’89, 1989.

Digital Library

Cited By

Castagna GLaurent MNguyễn K(2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632882
Marntirosian KSchrijvers TOliveira BKarachalias G(2020)Resolution as intersection subtyping via Modus PonensProceedings of the ACM on Programming Languages10.1145/34282744:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428274
Ye WSun YOliveira B(2024)Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional TypingProceedings of the ACM on Programming Languages10.1145/36897828:OOPSLA2(2010-2039)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689782
Show More Cited By

Index Terms

Disjoint intersection types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
      2. Language types
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs

Recommendations

Disjoint intersection types
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression ...
Gradual typing with union and intersection types

We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...
A Typed Lambda Calculus with Gradual Intersection Types
PPDP '22: Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming

Intersection types have the power to type expressions which are all of many different types. Gradual types combine type checking at both compile-time and run-time. Here we combine these two approaches in a new typed calculus that harness both of their ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 9

ICFP '16

September 2016

501 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3022670

Editor:
Matthew Fluet

Issue’s Table of Contents

ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
September 2016
501 pages
ISBN:9781450342193
DOI:10.1145/2951913
General Chairs:
Jacques Garrigue
Nagoya University, Japan
,
Gabriele Keller
University of New South Wales, Australia
,
Program Chair:
Eijiro Sumii
Tohoku University, Japan

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 September 2016

Published in SIGPLAN Volume 51, Issue 9

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
298
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)6

Reflects downloads up to 26 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Castagna GLaurent MNguyễn K(2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632882
Marntirosian KSchrijvers TOliveira BKarachalias G(2020)Resolution as intersection subtyping via Modus PonensProceedings of the ACM on Programming Languages10.1145/34282744:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428274
Ye WSun YOliveira B(2024)Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional TypingProceedings of the ACM on Programming Languages10.1145/36897828:OOPSLA2(2010-2039)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689782
Ye WOliveira BToro M(2024)Merging Gradual TypingProceedings of the ACM on Programming Languages10.1145/36897348:OOPSLA2(648-676)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689734
Rehman BOliveira BDi Stefano L(2024)Disjoint Polymorphism with Intersection and Union TypesProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686230(23-29)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686230
Tang WHillerström DMcKinna JSteuwer MDardha OFu RLindley S(2023)Structural Subtyping as Parametric PolymorphismProceedings of the ACM on Programming Languages10.1145/36228367:OOPSLA2(1093-1121)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622836
Saffrich HThiemann P(2023)Polymorphic Typestate for Session TypesProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610624(1-15)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610624
Xu HHuang XOliveira B(2023)Making a Type Difference: Subtraction on Intersection Types as Generalized Record OperationsProceedings of the ACM on Programming Languages10.1145/35712247:POPL(893-920)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571224
Rioux NHuang XOliveira BZdancewic S(2023)A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈Proceedings of the ACM on Programming Languages10.1145/35712117:POPL(515-543)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571211
Sun YDhandhania UOliveira B(2022)Compositional embeddings of domain-specific languagesProceedings of the ACM on Programming Languages10.1145/35632946:OOPSLA2(175-203)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563294
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents