research-article

Public Access

On the cost of type-tag soundness

Authors:

Ben Greenman,

Zeina MigeedAuthors Info & Claims

PEPM '18: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

Pages 30 - 39

https://doi.org/10.1145/3162066

Published: 25 December 2017 Publication History

PDF eReader

Abstract

Gradual typing systems ensure type soundness by transforming static type annotations into run-time checks. These checks provide semantic guarantees, but may come at a large cost in performance. In particular, recent work by Takikawa et al. suggests that enforcing a conventional form of type soundness may slow a program by two orders of magnitude.

Since different gradual typing systems satisfy different notions of soundness, the question then arises: what is the cost of such varying notions of soundness? This paper answers an instance of this question by applying Takikawa et al.'s evaluation method to Reticulated Python, which satisfies a notion of type-tag soundness. We find that the cost of soundness in Reticulated is at most one order of magnitude, and increases linearly with the number of type annotations.

References

[1]

Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, Robert Bruce Findler, Jan Vitek, and Matthias Felleisen. How to Evaluate the Performance of Gradual Type Systems. Submitted for publication, 2017.

Google Scholar

[2]

Fabian Muehlboeck and Ross Tate. Sound Gradual Typing is Nominally Alive and Well. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, 2017.

Digital Library

Google Scholar

[3]

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined Criteria for Gradual Typing. In Proc. Summit oN Advances in Programming Languages, 2015.

Google Scholar

[4]

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. Is Sound Gradual Typing Dead? In Proc. ACM Symposium on Principles of Programming Languages, pp. 456-468, 2016.

Digital Library

Google Scholar

[5]

Sam Tobin-Hochstadt and Matthias Felleisen. The Design and Implementation of Typed Scheme. In Proc. ACM Symposium on Principles of Programming Languages, pp. 395-406, 2008.

Digital Library

Google Scholar

[6]

Sam Tobin-Hochstadt, Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. Migratory Typing: Ten years later. In Proc. Summit oN Advances in Programming Languages, 2017.

Google Scholar

[7]

Michael M. Vitousek, Andrew Kent, Jeremy G. Siek, and Jim Baker. Design and Evaluation of Gradual Typing for Python. In Proc. Dynamic Languages Symposium, pp. 45-56, 2014.

Digital Library

Google Scholar

[8]

Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems. In Proc. ACM Symposium on Principles of Programming Languages, 2017.

Digital Library

Google Scholar

[9]

Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript. In Proc. European Conference on Object-Oriented Programming, pp. 28:1-28:29, 2017.

Google Scholar

Cited By

View all

Campora JKhan MChen S(2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632931
Greenman B(2023)GTP Benchmarks for Gradual Typing PerformanceProceedings of the 2023 ACM Conference on Reproducibility and Replicability10.1145/3589806.3600034(102-114)Online publication date: 27-Jun-2023
https://dl.acm.org/doi/10.1145/3589806.3600034
Greenwood-Thessman EGariano IRoberts RMarr SHomer MNoble JSeaton CFlückiger O(2021)Naïve transient cast insertion isn't (that) badProceedings of the 16th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems10.1145/3464972.3472395(1-9)Online publication date: 13-Jul-2021
https://dl.acm.org/doi/10.1145/3464972.3472395
Show More Cited By

Index Terms

On the cost of type-tag soundness
1. General and reference
  1. Cross-computing tools and techniques
    1. Metrics
2. Software and its engineering
  1. Software creation and management
    1. Software post-development issues
      1. Software evolution

Recommendations

A spectrum of type soundness and performance

The literature on gradual typing presents three fundamentally different ways of thinking about the integrity of programs that combine statically typed and dynamically typed code. This paper presents a uniform semantic framework that explains all three ...
Collapsible contracts: fixing a pathology of gradual typing

The promise of gradual typing is that programmers should get the best of both worlds: the static guarantees of static types, and the dynamic flexibility of untyped programming. This is an enticing benefit, but one that, in practice, may carry significant ...
Type soundness for dependent object types (DOT)
OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

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

PEPM '18: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

December 2017

73 pages

ISBN:9781450355872

DOI:10.1145/3175493

Program Chairs:
Fritz Henglein
University of Copenhagen, Denmark
,
Hsiang-Shang Ko
National Institute of Informatics, Japan

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].

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 December 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

POPL '18

Sponsor:

SIGPLAN

POPL '18: The 45th Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 8 - 9, 2018

CA, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 66 of 120 submissions, 55%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
203
Total Downloads

Downloads (Last 12 months)55
Downloads (Last 6 weeks)8

Reflects downloads up to 23 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Campora JKhan MChen S(2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632931
Greenman B(2023)GTP Benchmarks for Gradual Typing PerformanceProceedings of the 2023 ACM Conference on Reproducibility and Replicability10.1145/3589806.3600034(102-114)Online publication date: 27-Jun-2023
https://dl.acm.org/doi/10.1145/3589806.3600034
Greenwood-Thessman EGariano IRoberts RMarr SHomer MNoble JSeaton CFlückiger O(2021)Naïve transient cast insertion isn't (that) badProceedings of the 16th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems10.1145/3464972.3472395(1-9)Online publication date: 13-Jul-2021
https://dl.acm.org/doi/10.1145/3464972.3472395
Moy CNguyễn PTobin-Hochstadt SVan Horn D(2021)Corpse reviver: sound and efficient gradual typing via contract verificationProceedings of the ACM on Programming Languages10.1145/34343345:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434334
SIEK JCHEN T(2021)Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculiJournal of Functional Programming10.1017/S095679682100024131Online publication date: 11-Nov-2021
https://doi.org/10.1017/S0956796821000241
Tunnell Wilson PGreenman BPombrio JKrishnamurthi S(2020)The behavior of gradual types: a user studyACM SIGPLAN Notices10.1145/3393673.327694753:8(1-12)Online publication date: 6-Apr-2020
https://dl.acm.org/doi/10.1145/3393673.3276947
Vitousek MSiek JChaudhuri AMarr SFumero J(2019)Optimizing and evaluating transient gradual typingProceedings of the 15th ACM SIGPLAN International Symposium on Dynamic Languages10.1145/3359619.3359742(28-41)Online publication date: 20-Oct-2019
https://dl.acm.org/doi/10.1145/3359619.3359742
Kuhlenschmidt AAlmahallawi DSiek JMcKinley KFisher K(2019)Toward efficient gradual typing for structural types via coercionsProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314627(517-532)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314627
GREENMAN BTAKIKAWA ANEW MFELTEY DFINDLER RVITEK JFELLEISEN M(2019)How to evaluate the performance of gradual type systemsJournal of Functional Programming10.1017/S095679681800021729Online publication date: 20-Feb-2019
https://doi.org/10.1017/S0956796818000217
Tunnell Wilson PGreenman BPombrio JKrishnamurthi SFelgentreff T(2018)The behavior of gradual types: a user studyProceedings of the 14th ACM SIGPLAN International Symposium on Dynamic Languages10.1145/3276945.3276947(1-12)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276945.3276947
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Cited By

Index Terms

Recommendations

A spectrum of type soundness and performance

Collapsible contracts: fixing a pathology of gradual typing

Type soundness for dependent object types (DOT)