research-article

Open access

Undecidability of d_<: and its decidable fragments

Authors:

Jason Z. S. Hu,

Ondřej LhotákAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue POPL

Article No.: 9, Pages 1 - 30

https://doi.org/10.1145/3371077

Published: 20 December 2019 Publication History

Abstract

Dependent Object Types (DOT) is a calculus with path dependent types, intersection types, and object self-references, which serves as the core calculus of Scala 3. Although the calculus has been proven sound, it remains open whether type checking in DOT is decidable. In this paper, we establish undecidability proofs of type checking and subtyping of D_<:, a syntactic subset of DOT. It turns out that even for D_<:, undecidability is surprisingly difficult to show, as evidenced by counterexamples for past attempts. To prove undecidability, we discover an equivalent definition of the D_<: subtyping rules in normal form. Besides being easier to reason about, this definition makes the phenomenon of subtyping reflection explicit as a single inference rule. After removing this rule, we discover two decidable fragments of D_<: subtyping and identify algorithms to decide them. We prove soundness and completeness of the algorithms with respect to the fragments, and we prove that the algorithms terminate. Our proofs are mechanized in a combination of Coq and Agda.

Supplementary Material

WEBM File (a9-hu.webm)

Download
82.57 MB

References

[1]

Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella (Eds.), Vol. 9600. Springer, 249–272.

[2]

Nada Amin, Adriaan Moors, and Martin Odersky. 2012. Dependent object types. In 19th International Workshop on Foundations of Object-Oriented Languages.

[3]

Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. ACM, 666–679. http://dl.acm.org/citation.cfm?id=3009866

Digital Library

[4]

Nada Amin, Tiark Rompf, and Martin Odersky. 2014. Foundations of Path-dependent Types. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA ’14). ACM, New York, NY, USA, 233–249.

Digital Library

[5]

David Aspinall and Adriana Compagnoni. 2001. Subtyping dependent types. Theoretical Computer Science 266, 1 (2001), 273 – 309.

Digital Library

[6]

Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics, Vol. 103. North-Holland.

[7]

L. Cardelli, S. Martini, J.C. Mitchell, and A. Scedrov. 1994. An Extension of System F with Subtyping. Information and Computation 109, 1 (1994), 4 – 56.

Digital Library

[8]

Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. ACM Comput. Surv. 17, 4 (Dec. 1985), 471–523.

Digital Library

[9]

Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press.

Digital Library

[10]

Pierre-Louis Curien and Giorgio Ghelli. 1990. Coherence of Subsumption. In CAAP ’90, 15th Colloquium on Trees in Algebra and Programming, Copenhagen, Denmark, May 15-18, 1990, Proceedings (Lecture Notes in Computer Science), André Arnold (Ed.), Vol. 431. Springer, 132–146.

[11]

Yannick Forster, Edith Heiter, and Gert Smolka. 2018. Verification of PCP-Related Computational Reductions in Coq. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Oxford, UK, July 9-12, 2018 (LNCS 10895). Springer, 253–269. Preliminary version appeared as arXiv:1711.07023.

[12]

Yannick Forster and Dominique Larchey-Wendling. 2019. Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019). ACM, New York, NY, USA, 104–117.

Digital Library

[13]

Yannick Forster and Gert Smolka. 2017. Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. In Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings (Lecture Notes in Computer Science), Mauricio Ayala-Rincón and César A. Muñoz (Eds.), Vol. 10499. Springer, 189–206.

[14]

Ben Greenman, Fabian Muehlboeck, and Ross Tate. 2014. Getting F-bounded polymorphism into shape. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, Michael F. P. O’Boyle and Keshav Pingali (Eds.). ACM, 89–99.

Digital Library

[15]

Radu Grigore. 2017. Java generics are turing complete. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 73–85. http://dl.acm.org/citation.cfm?id=3009871

Digital Library

[16]

Zhong Sheng Hu. 2019. Decidability and Algorithmic Analysis of Dependent Object Types (DOT). Master’s thesis. University of Waterloo. http://hdl.handle.net/10012/14964

[17]

Andrew Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with Variance. In International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD) (international workshop on foundations and developments of object-oriented languages (fool/wood) ed.). https://www.microsoft.com/enus/research/publication/on- decidability- of- nominal- subtyping- with- variance/

[18]

Julian Mackay, Alex Potanin, Lindsay Groves, and Jonathan Aldrich. 2020. Decidable Subtyping for Path Dependent Types. In Proceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2020, New Orleans, USA, January 22-24, 2020.

Digital Library

[19]

John C. Martin. 1997. Introduction to Languages and the Theory of Computation (2nd ed.). McGraw-Hill Higher Education.

[20]

Abel Nieto. 2017. Towards Algorithmic Typing for DOT (Short Paper). In Proceedings of the 8th ACM SIGPLAN International Symposium on Scala (SCALA 2017). ACM, New York, NY, USA, 2–7.

Digital Library

[21]

Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger. 2003. A Nominal Theory of Objects with Dependent Types. In ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, Germany, July 21-25, 2003, Proceedings (Lecture Notes in Computer Science), Luca Cardelli (Ed.), Vol. 2743. Springer, 201–224.

[22]

Frank Pfenning. 2000. Structural Cut Elimination: I. Intuitionistic and Classical Logic. Information and Computation 157, 1 (2000), 84 – 141.

Digital Library

[23]

Benjamin C. Pierce. 1991. Programming with intersection types and bounded polymorphism. Ph.D. Dissertation. Carnegie Mellon University.

Digital Library

[24]

Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’92). ACM, New York, NY, USA, 305–315.

Digital Library

[25]

Benjamin C. Pierce. 1997. Bounded Quantification with Bottom. Technical Report 492. Computer Science Department, Indiana University.

[26]

Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press.

Digital Library

[27]

Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press.

Digital Library

[28]

Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták. 2017. A Simple Soundness Proof for Dependent Object Types. Proc. ACM Program. Lang. 1, OOPSLA, Article 46 (Oct. 2017), 27 pages.

Digital Library

[29]

Tiark Rompf and Nada Amin. 2016. Type Soundness for Dependent Object Types (DOT). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016). ACM, New York, NY, USA, 624–641.

Digital Library

[30]

Agda Team. 2019. Agda 2.5.4.2.

[31]

The Coq Development Team. 2018. The Coq Proof Assistant, version 8.8.2.

[32]

Stefan Wehr and Peter Thiemann. 2009. On the Decidability of Subtyping with Bounded Existential Types. In Proceedings of the 7th Asian Symposium on Programming Languages and Systems (APLAS ’09). Springer-Verlag, Berlin, Heidelberg, 111–127.

Digital Library

Cited By

Belyakova JChung BTate RVitek J(2024)Decidable Subtyping of Existential Types for JuliaProceedings of the ACM on Programming Languages10.1145/36564218:PLDI(1091-1114)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656421
Zhou LZhou YOliveira B(2023)Recursive Subtyping for AllProceedings of the ACM on Programming Languages10.1145/35712417:POPL(1396-1425)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571241
Ding SZhang Q(2023)Witnessability of Undecidable ProblemsProceedings of the ACM on Programming Languages10.1145/35712277:POPL(982-1002)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571227
Show More Cited By

Index Terms

Undecidability of d_<: and its decidable fragments
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Logic
    1. Type theory

Recommendations

Towards algorithmic typing for DOT (short paper)
SCALA 2017: Proceedings of the 8th ACM SIGPLAN International Symposium on Scala

The Dependent Object Types (DOT) calculus formalizes key features of Scala. The D_<: calculus is the core of DOT. To date, presentations of D_<: have used declarative, as opposed to algorithmic, typing and subtyping rules. Unfortunately, algorithmic ...
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
CSL '08: Proceedings of the 22nd international workshop on Computer Science Logic

This paper shows undecidability of type-checking and type-inference problems in domain-free typed lambda-calculi with existential types: a negation and conjunction fragment, and an implicational fragment. These are proved by reducing type-checking and ...
The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types

We consider here a number of variations on System F that are predicative second-order systems whose terms are intermediate between the Curry style and the Church style. As in the Church style, the terms we deal with here contain the information on where ...

Comments

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 4, Issue POPL

January 2020

1984 pages

EISSN:2475-1421

DOI:10.1145/3377388

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 December 2019

Published in PACMPL Volume 4, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
859
Total Downloads

Downloads (Last 12 months)86
Downloads (Last 6 weeks)17

Reflects downloads up to 21 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Belyakova JChung BTate RVitek J(2024)Decidable Subtyping of Existential Types for JuliaProceedings of the ACM on Programming Languages10.1145/36564218:PLDI(1091-1114)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656421
Zhou LZhou YOliveira B(2023)Recursive Subtyping for AllProceedings of the ACM on Programming Languages10.1145/35712417:POPL(1396-1425)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571241
Ding SZhang Q(2023)Witnessability of Undecidable ProblemsProceedings of the ACM on Programming Languages10.1145/35712277:POPL(982-1002)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571227
Boruch-Gruszecki AWaśko RXu YParreaux L(2022)A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoningProceedings of the ACM on Programming Languages10.1145/35633426:OOPSLA2(1526-1555)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563342
Zhou YOliveira BFan A(2022)A Calculus with Recursive Types, Record Concatenation and SubtypingProgramming Languages and Systems10.1007/978-3-031-21037-2_9(175-195)Online publication date: 25-Nov-2022
https://doi.org/10.1007/978-3-031-21037-2_9
Xu YBoruch-Gruszecki AParreaux LRichard-Foy JDoeraene S(2021)Implementing path-dependent GADT reasoning for Scala 3Proceedings of the 12th ACM SIGPLAN International Symposium on Scala10.1145/3486610.3486892(22-32)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1145/3486610.3486892
Stucki SGiarrusso P(2021)A theory of higher-order subtyping with type intervalsProceedings of the ACM on Programming Languages10.1145/34735745:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473574

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents