research-article

Type soundness for dependent object types (DOT)

Authors:

Nada AminAuthors Info & Claims

OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

Pages 624 - 641

https://doi.org/10.1145/2983990.2984008

Published: 19 October 2016 Publication History

Abstract

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. Unfortunately, type soundness has only been established for restricted subsets of DOT. In fact, it has been shown that important Scala features such as type refinement or a subtyping relation with lattice structure break at least one key metatheoretic property such as environment narrowing or invertible subtyping transitivity, which are usually required for a type soundness proof. The main contribution of this paper is to demonstrate how, perhaps surprisingly, even though these properties are lost in their full generality, a rich DOT calculus that includes recursive type refinement and a subtyping lattice with intersection types can still be proved sound. The key insight is that subtyping transitivity only needs to be invertible in code paths executed at runtime, with contexts consisting entirely of valid runtime objects, whereas inconsistent subtyping contexts can be permitted for code that is never executed.

References

[1]

M. S. Ager, D. Biernacki, O. Danvy, and J. Midtgaard. A functional correspondence between evaluators and abstract machines. In PPDP, 2003.

Digital Library

[2]

N. Amin. Dependent Object Types. PhD thesis, EPFL, 2016.

[3]

N. Amin, S. Grütter, M. Odersky, T. Rompf, and S. Stucki. The essence of dependent object types. In WadlerFest, A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, 2016.

[4]

N. Amin, A. Moors, and M. Odersky. Dependent object types. In FOOL, 2012.

[5]

N. Amin, T. Rompf, and M. Odersky. Foundations of pathdependent types. In OOPSLA, 2014.

Digital Library

[6]

N. Amin and R. Tate. Java and Scala’s type systems are unsound: the existential crisis of null pointers. In OOPSLA, 2016.

Digital Library

[7]

B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanized metatheory for the masses: The PoplMark Challenge. In TPHOLs, 2005.

Digital Library

[8]

N. R. Cameron, J. Noble, and T. Wrigstad. Tribal ownership. In OOPSLA, 2010.

Digital Library

[9]

L. Cardelli, S. Martini, J. C. Mitchell, and A. Scedrov. An extension of system F with subtyping. Inf. Comput., 109(1/2):4– 56, 1994.

Digital Library

[10]

D. Clarke, S. Drossopoulou, J. Noble, and T. Wrigstad. Tribe: a simple virtual class calculus. In AOSD, 2007.

Digital Library

[11]

V. Cremet, F. Garillot, S. Lenglet, and M. Odersky. A core calculus for Scala type checking. In MFCS, 2006.

Digital Library

[12]

O. Danvy and J. Johannsen. Inter-deriving semantic artifacts for object-oriented programming. J. Comput. Syst. Sci., 76(5):302–323, 2010.

Digital Library

[13]

O. Danvy, K. Millikin, J. Munk, and I. Zerny. On interderiving small-step and big-step semantics: A case study for storeless call-by-need evaluation. Theor. Comput. Sci., 435:21–42, 2012.

Digital Library

[14]

D. Dreyer and A. Rossberg. Mixin’ up the ML module system. In ICFP, 2008.

Digital Library

[15]

E. Ernst. Family polymorphism. In ECOOP, 2001.

Digital Library

[16]

E. Ernst. Higher-order hierarchies. In ECOOP, 2003.

[17]

E. Ernst, K. Ostermann, and W. R. Cook. A virtual class calculus. In POPL, 2006.

Digital Library

[18]

C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In PLDI, 1993.

Digital Library

[19]

V. Gasiunas, M. Mezini, and K. Ostermann. Dependent classes. In OOPSLA, 2007.

Digital Library

[20]

J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. 1972.

[21]

R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In POPL, 1994.

Digital Library

[22]

A. Igarashi, B. C. Pierce, and P. Wadler. Featherweight java: a minimal core calculus for java and gj. ACM Trans. Program. Lang. Syst., 23(3), 2001.

Digital Library

[23]

T. Jones, M. Homer, and J. Noble. Brand objects for nominal typing. In ECOOP, 2015.

[24]

X. Leroy. Manifest types, modules and separate compilation. In POPL, 1994.

Digital Library

[25]

D. Macqueen. Using dependent types to express modular structure. In POPL, 1986.

Digital Library

[26]

A. Moors, F. Piessens, and M. Odersky. Safe type-level abstraction in Scala. In FOOL, 2008.

[27]

N. Nystrom, S. Chong, and A. C. Myers. Scalable extensibility via nested inheritance. In OOPSLA, 2004.

Digital Library

[28]

M. Odersky. The trouble with types. Presentation at Strange Loop, 2013.

[29]

M. Odersky. The essence of Scala. http://www.scala-lang. org/blog/2016/02/03/essence-of-scala.html, February 2016.

[30]

M. Odersky, V. Cremet, C. Röckl, and M. Zenger. A nominal theory of objects with dependent types. In ECOOP, 2003.

[31]

M. Odersky and K. Läufer. Putting type annotations to work. In POPL, 1996.

Digital Library

[32]

M. Odersky and T. Rompf. Unifying functional and objectoriented programming with Scala. Commun. ACM, 57(4):76– 86, 2014.

Digital Library

[33]

B. C. Pierce. Types and programming languages. MIT Press, 2002.

Digital Library

[34]

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

Digital Library

[35]

J. C. Reynolds. Towards a theory of type structure. In Symposium on Programming, volume 19 of Lecture Notes in Computer Science, pages 408–423. Springer, 1974.

Digital Library

[36]

T. Rompf and N. Amin. From F to DOT: Type soundness proofs with definitional interpreters. Technical report, Purdue University, July 2015. http://arxiv.org/abs/1510.05216.

[37]

A. Rossberg. 1ML - core and modules united (f-ing first-class modules). In ICFP, 2015.

Digital Library

[38]

A. Rossberg, C. V. Russo, and D. Dreyer. F-ing modules. J. Funct. Program., 24(5):529–607, 2014.

[39]

A. J. Summers. Modelling java requires state. In Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, page 10. ACM, 2009.

Digital Library

[40]

G. A. Washburn. SI-1557: Another type soundness hole. https://issues.scala-lang.org/browse/SI-1557, 2008.

[41]

A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38–94, 1994.

Digital Library

Cited By

Tan JOliveira B(2024)A Case for First-Class EnvironmentsProceedings of the ACM on Programming Languages10.1145/36898008:OOPSLA2(2521-2550)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689800
Zhou LWan QOliveira B(2024)Full Iso-Recursive TypesProceedings of the ACM on Programming Languages10.1145/36897188:OOPSLA2(192-221)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689718
Racordon DLaemmel RPereira JMosses P(2024)Type Checking with Rewriting RulesProceedings of the 17th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3687997.3695640(171-183)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3687997.3695640
Show More Cited By

Index Terms

Type soundness for dependent object types (DOT)
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

Type soundness proofs with definitional interpreters
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

October 2016

915 pages

ISBN:9781450344449

DOI:10.1145/2983990

General Chair:
Eelco Visser
Delft University of Technology, Netherlands
,
Program Chair:
Yannis Smaragdakis
University of Athens, Greece

ACM SIGPLAN Notices Volume 51, Issue 10
OOPSLA '16
October 2016
915 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3022671
Editor:
Matthew Fluet
Issue’s Table of Contents

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 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: 19 October 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '16

Sponsor:

SIGPLAN

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

November 2 - 4, 2016

Amsterdam, Netherlands

Acceptance Rates

Overall Acceptance Rate 268 of 1,244 submissions, 22%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
374
Total Downloads

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

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tan JOliveira B(2024)A Case for First-Class EnvironmentsProceedings of the ACM on Programming Languages10.1145/36898008:OOPSLA2(2521-2550)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689800
Zhou LWan QOliveira B(2024)Full Iso-Recursive TypesProceedings of the ACM on Programming Languages10.1145/36897188:OOPSLA2(192-221)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689718
Racordon DLaemmel RPereira JMosses P(2024)Type Checking with Rewriting RulesProceedings of the 17th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3687997.3695640(171-183)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3687997.3695640
Racordon DFlesselle EBovel MErtl MKirsch C(2024)Existential Containers in ScalaProceedings of the 21st ACM SIGPLAN International Conference on Managed Programming Languages and Runtimes10.1145/3679007.3685056(55-64)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679007.3685056
Boruch-Gruszecki AOdersky MLee ELhoták OBrachthäuser J(2023)Capturing TypesACM Transactions on Programming Languages and Systems10.1145/361800345:4(1-52)Online publication date: 20-Nov-2023
https://dl.acm.org/doi/10.1145/3618003
Charguéraud AChlipala AErbsen AGruetter S(2023)Omnisemantics: Smooth Handling of NondeterminismACM Transactions on Programming Languages and Systems10.1145/357983445:1(1-43)Online publication date: 8-Mar-2023
https://dl.acm.org/doi/10.1145/3579834
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
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
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
Blaudeau CLiu F(2022)A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius modelProceedings of the ACM on Programming Languages10.1145/35633146:OOPSLA2(729-757)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563314
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.

Media

Figures

Other

Tables

View Table of Contents