research-article

Confined gradual typing

Authors:

Esteban Allende,

Éric TanterAuthors Info & Claims

OOPSLA '14: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications

Pages 251 - 270

https://doi.org/10.1145/2660193.2660222

Published: 15 October 2014 Publication History

Abstract

Gradual typing combines static and dynamic typing flexibly and safely in a single programming language. To do so, gradually typed languages implicitly insert casts where needed, to ensure at runtime that typing assumptions are not violated by untyped code. However, the implicit nature of cast insertion, especially on higher-order values, can jeopardize reliability and efficiency: higher-order casts can fail at any time, and are costly to execute. We propose Confined Gradual Typing, which extends gradual typing with two new type qualifiers that let programmers control the flow of values between the typed and the untyped worlds, and thereby trade some flexibility for more reliability and performance. We formally develop two variants of Confined Gradual Typing that capture different flexibility/guarantee tradeoffs. We report on the implementation of Confined Gradual Typing in Gradualtalk, a gradually-typed Smalltalk, which confirms the performance advantage of avoiding unwanted higher-order casts and the low overhead of the approach.

References

[1]

E. Allende, O. Callaú, J. Fabry, É. Tanter, and M. Denker. Gradual typing for Smalltalk. Science of Computer Programming, Aug. 2013. Available online.

[2]

E. Allende, J. Fabry, and É. Tanter. Cast insertion strategies for gradually-typed objects. In Proceedings of the 9th ACM Dynamic Languages Symposium (DLS 2013), pages 27--36, Indianapolis, IN, USA, Oct. 2013. ACM Press. ACM SIGPLAN Notices, 49(2).

Digital Library

[3]

E. Allende, J. Fabry, R. Garcia, and É. Tanter. Confined gradual typing -- extended version with detailed proofs. Technical Report TR/DCC-2014--3, University of Chile, May 2014.

[4]

B. Bloom, J. Field, N. Nystrom, J. Östlund, G. Richards, R. Strnisa, J. Vitek, and T. Wrigstad. Thorn: robust, concurrent, extensible scripting on the JVM. In Proceedings of the 24th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2009), pages 117--136, Orlando, Florida, USA, Oct. 2009. ACM Press.

Digital Library

[5]

G. Bracha. Pluggable type systems. In OOPSLA Workshop on Revival of Dynamic Languages, pages 1--6, 2004.

[6]

G. Bracha and D. Griswold. Strongtalk: Typechecking Smalltalk in a production environment. In Proceedings of the 8th International Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 95), pages 215--230, Washington, D.C., USA, Oct. 1993. ACM Press. ACM SIGPLAN Notices, 28(10).

Digital Library

[7]

R. Cartwright and M. Fagan. Soft typing. In Proceedings of the ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), pages 278--292, Toronto, Ontario, Canada, 1991.

Digital Library

[8]

G. Castagna, editor. Proceedings of the 18th European Symposium on Programming Languages and Systems (ESOP 2009), volume 5502 of phLecture Notes in Computer Science, York, UK, 2009. Springer-Verlag.

Digital Library

[9]

R. B. Findler and M. Felleisen. Contracts for higher-order functions. In Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming, pages 48--59, Pittsburgh, PA, USA, 2002. ACM Press.

Digital Library

[10]

M. Furr. Combining Static and Dynamic Typing in Ruby. PhD thesis, University of Maryland, 2009.

[11]

D. Grossman, G. Morrisett, and S. Zdancewic. Syntactic type abstraction. ACM Transactions on Programming Languages and Systems, 22 (6): 1037--1080, Nov. 2000.

Digital Library

[12]

D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. Higher-Order and Sympolic Computation, 23 (2): 167--189, June 2010.

Digital Library

[13]

L. Ina and A. Igarashi. Gradual typing for generics. In Proceedings of the 26th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2011), pages 609--624, Portland, Oregon, USA, Oct. 2011. ACM Press.

Digital Library

[14]

K. Knowles and C. Flanagan. Hybrid type checking. ACM Transactions on Programming Languages and Systems, 32 (2): Article n.6, Jan. 2010.

Digital Library

[15]

J. Matthews and R. B. Findler. Operational semantics for multi-language programs. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), pages 3--10, Nice, France, Jan. 2007. ACM Press.

Digital Library

[16]

POPL 2010. Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2010), Madrid, Spain, Jan. 2010. ACM Press.

[17]

A. Rastogi, A. Chaudhuri, and B. Hosmer. The ins and outs of gradual type inference. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2012), pages 481--494, Philadelphia, USA, Jan. 2012. ACM Press.

Digital Library

[18]

B. V. Ryseghem, S. Ducasse, and J. Fabry. Seamless composition and reuse of customizable user interfaces with Spec. Science of Computer Programming, 2014. To appear.

Digital Library

[19]

J. Siek and W. Taha. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop, pages 81--92, Sept. 2006.

[20]

J. Siek and W. Taha. Gradual typing for objects. In E. Ernst, editor, Proceedings of the 21st European Conference on Object-oriented Programming (ECOOP 2007), number 4609 in Lecture Notes in Computer Science, pages 2--27, Berlin, Germany, July 2007. Springer-Verlag.

Digital Library

[21]

J. Siek and P. Wadler. Threesomes, with and without blame. Incitetpopl2010, pages 365--376.

Digital Library

[22]

J. Siek, R. Garcia, and W. Taha. Exploring the design space of higher-order casts. Incitetesop2009, pages 17--31.

Digital Library

[23]

N. Swamy, C. Fournet, A. Rastogi, K. Bhargavan, J. Chen, P.-Y. Strub, and G. Bierman. Gradual typing embedded securely in JavaScript. In Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2014), pages 425--437, San Diego, CA, USA, Jan. 2014. ACM Press.

Digital Library

[24]

A. Takikawa, T. S. Strickland, C. Dimoulas, S. Tobin-Hochstadt, and M. Felleisen. Gradual typing for first-class classes. In Proceedings of the 27th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2012), pages 793--810, Tucson, AZ, USA, Oct. 2012. ACM Press.

Digital Library

[25]

S. Tobin-Hochstadt. Typed Scheme: From Scripts to Programs. PhD thesis, Northeastern University, Jan. 2010.

[26]

S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: from scripts to programs. In Proceedings of the ACM Dynamic Languages Symposium (DLS 2006), pages 964--974, Portland, Oregon, USA, Oct. 2006. ACM Press.

Digital Library

[27]

P. Wadler and R. B. Findler. Well-typed programs can't be blamed. Incitetesop2009, pages 1--16.

Digital Library

[28]

T. Wrigstad, F. Zappa Nardelli, S. Lebresne, J. Östlund, and J. Vitek. Integrating typed and untyped code in a scripting language. Incitetpopl2010, pages 377--388.

Digital Library

Cited By

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
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
Show More Cited By

Index Terms

Confined gradual typing
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

Gradual typing: a new perspective

We define a new, more semantic interpretation of gradual types and use it to ``gradualize'' two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism. In particular, we use the new interpretation to define three gradual type ...
Abstracting gradual typing
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory ...
Confined gradual typing
OOPSLA '14

Gradual typing combines static and dynamic typing flexibly and safely in a single programming language. To do so, gradually typed languages implicitly insert casts where needed, to ensure at runtime that typing assumptions are not violated by untyped ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA '14: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications

October 2014

946 pages

ISBN:9781450325851

DOI:10.1145/2660193

General Chair:
Andrew Black
Portland State University, USA
,
Program Chair:
Todd Millstein
University of California, Los Angeles, USA

ACM SIGPLAN Notices Volume 49, Issue 10
OOPSLA '14
October 2014
907 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2714064
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2014 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: 15 October 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Fondo Nacional de Desarrollo Científico y Tecnológico

Conference

SPLASH '14

Sponsor:

SIGPLAN

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

October 20 - 24, 2014

Oregon, Portland, USA

Acceptance Rates

OOPSLA '14 Paper Acceptance Rate 52 of 186 submissions, 28%;

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

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
349
Total Downloads

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

Reflects downloads up to 29 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
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
Zolfagharinia MAdams BGuéhéneuc Y(2019)A study of build inflation in 30 million CPAN builds on 13 Perl versions and 10 operating systemsEmpirical Software Engineering10.1007/s10664-019-09709-624:6(3933-3971)Online publication date: 19-Jun-2019
https://doi.org/10.1007/s10664-019-09709-6
Zhang JTan CLv Q(2018)"This is why we play"Proceedings of the ACM on Human-Computer Interaction10.1145/32744662:CSCW(1-25)Online publication date: 1-Nov-2018
https://dl.acm.org/doi/10.1145/3274466
Gui XChen YPine K(2018)Navigating the Healthcare Service "Black Box"Proceedings of the ACM on Human-Computer Interaction10.1145/32743302:CSCW(1-26)Online publication date: 1-Nov-2018
https://dl.acm.org/doi/10.1145/3274330
Greenman BFelleisen M(2018)A spectrum of type soundness and performanceProceedings of the ACM on Programming Languages10.1145/32367662:ICFP(1-32)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236766
Yang SLin BXu J(2017)Safe Randomized Load-Balanced Switching By Diffusing Extra LoadsProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/31544871:2(1-37)Online publication date: 19-Dec-2017
https://dl.acm.org/doi/10.1145/3154487
Jafery KDunfield J(2017)Sums of uncertainty: refinements go gradualACM SIGPLAN Notices10.1145/3093333.300986552:1(804-817)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009865
Jafery KDunfield JCastagna GGordon A(2017)Sums of uncertainty: refinements go gradualProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009865(804-817)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009865
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