research-article

Towards algorithmic typing for DOT (short paper)

Author:

Abel NietoAuthors Info & Claims

SCALA 2017: Proceedings of the 8th ACM SIGPLAN International Symposium on Scala

Pages 2 - 7

https://doi.org/10.1145/3136000.3136003

Published: 22 October 2017 Publication History

Abstract

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 typing for full D_<: is known to be an undecidable problem.

We explore the design space for a restricted version of D_<: that has decidable typechecking. Even in this simplified D_<:, algorithmic typing and subtyping are tricky, due to the "bad bounds" problem. The Scala compiler bypasses bad bounds at the cost of a loss in expressiveness in its type system. Based on the approach taken in the Scala compiler, we present the Step Typing and Step Subtyping relations for D_<:. These relations are sound and decidable. They are not complete with respect to the original D_<: typing rules.

References

[1]

Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. Springer International Publishing, Cham.

[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, 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 2014. 233-249.

Digital Library

[4]

Nada Amin and Ross Tate. 2016. Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers. In to appear in OOPSLA 2016.

Digital Library

[5]

Runar Bjarnason. 2009. More Scala Typehackery. (2009). https://apocalisp.wordpress.com/2009/09/02/ Accessed: 2017-07-15.

[6]

Runar Bjarnason. 2011. Simple SKI Combinator Calculus in Scala's Type System. (2011). https://apocalisp.wordpress.com/2011/01/13/simple-ski-combinator-calculus-in-scalas-type-system/ Accessed: 2017-07-15.

[7]

Luca Cardelli, Simone Martini, John C Mitchell, and Andre Scedrov. 1994. An extension of system F with subtyping. Information and Computation 109, 1-2 (1994), 4-56.

Digital Library

[8]

Luca Cardelli and Peter Wegner. 1985. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys (CSUR) 17, 4 (1985), 471-523.

Digital Library

[9]

Vincent Cremet, François Garillot, Sergueï Lenglet, and Martin Odersky. 2006. A Core Calculus for Scala Type Checking. In Mathematical Foundations of Computer Science, 31st International Symposium, Slovakia.

Digital Library

[10]

Abel Nieto. 2017. Towards Algorithmic Typing for DOT. CoRR abs/1708.05437 (2017). http://arxiv.org/abs/1708.05437

[11]

Martin Odersky. 2016. Scaling DOT to Scala -- Soundness. http://www.scala-lang.org/blog/2016/02/17/scaling-dot-soundness.html. (2016).

[12]

Benjamin C Pierce. 1994. Bounded quantification is undecidable. Information and Computation 112, 1 (1994), 131-165.

Digital Library

[13]

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

Digital Library

[14]

Benjamin C Pierce and David N Turner. 2000. Local type inference. ACM Transactions on Programming Languages and Systems (TOPLAS) 22, 1 (2000), 1-44.

Digital Library

[15]

Marianna Rapoport, Ifaz Kabir, Paul He, and Ondrej Lhoták. 2017. A Simple Soundness Proof for Dependent Object Types. In Proceedings of the 2017 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2017. To appear.

Digital Library

[16]

Tiark Rompf and Nada Amin. 2015. From F to DOT: Type Soundness Proofs with Definitional Interpreters. CoRR abs/1510.05216v1 (2015). http://arxiv.org/abs/1510.05216v1

Cited By

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
Giarrusso PStefanesco LTimany ABirkedal LKrebbers R(2020)Scala step-by-step: soundness for DOT with step-indexed logical relations in IrisProceedings of the ACM on Programming Languages10.1145/34089964:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408996
Mackay JPotanin AAldrich JGroves L(2019)Decidable subtyping for path dependent typesProceedings of the ACM on Programming Languages10.1145/33711344:POPL(1-27)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371134
Show More Cited By

Index Terms

Towards algorithmic typing for DOT (short paper)
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages

Recommendations

Undecidability of d_<: and its decidable fragments

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 ...
A simple soundness proof for dependent object types

Dependent Object Types (DOT) is intended to be a core calculus for modelling Scala. Its distinguishing feature is abstract type members, fields in objects that hold types rather than values. Proving soundness of DOT has been surprisingly challenging, ...
Type soundness for dependent object types (DOT)
OOPSLA '16

Scala’s type system unifies aspects of ML modules, object- oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

SCALA 2017: Proceedings of the 8th ACM SIGPLAN International Symposium on Scala

October 2017

77 pages

ISBN:9781450355292

DOI:10.1145/3136000

General Chair:
Heather Miller
EPFL, Switzerland / Northeastern University, USA
,
Program Chairs:
Philipp Haller
KTH, Sweden
,
Ondřej Lhoták
University of Waterloo, Canada

Copyright © 2017 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 the author(s) 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].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGAda: ACM Special Interest Group on Ada Programming Language

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 October 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '17

Sponsor:

SIGPLAN

SPLASH '17: Conference on Systems, Programming, Languages, and Applications: Software for Humanity

October 22 - 23, 2017

BC, Vancouver, Canada

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
138
Total Downloads

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

Reflects downloads up to 21 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Giarrusso PStefanesco LTimany ABirkedal LKrebbers R(2020)Scala step-by-step: soundness for DOT with step-indexed logical relations in IrisProceedings of the ACM on Programming Languages10.1145/34089964:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408996
Mackay JPotanin AAldrich JGroves L(2019)Decidable subtyping for path dependent typesProceedings of the ACM on Programming Languages10.1145/33711344:POPL(1-27)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371134
Hu JLhoták O(2019)Undecidability of d and its decidable fragmentsProceedings of the ACM on Programming Languages10.1145/33710774:POPL(1-30)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371077
Parreaux LBoruch-Gruszecki AGiarrusso PBrachthäuser JRyu SNystrom N(2019)Towards improved GADT reasoning in ScalaProceedings of the Tenth ACM SIGPLAN Symposium on Scala10.1145/3337932.3338813(12-16)Online publication date: 17-Jul-2019
https://dl.acm.org/doi/10.1145/3337932.3338813

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents