research-article

Blame for all

Authors:

Robert Bruce Findler,

Jeremy G. Siek,

Philip WadlerAuthors Info & Claims

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 201 - 214

https://doi.org/10.1145/1926385.1926409

Published: 26 January 2011 Publication History

Abstract

Several programming languages are beginning to integrate static and dynamic typing, including Racket (formerly PLT Scheme), Perl 6, and C# 4.0 and the research languages Sage (Gronski, Knowles, Tomb, Freund, and Flanagan, 2006) and Thorn (Wrigstad, Eugster, Field, Nystrom, and Vitek, 2009). However, an important open question remains, which is how to add parametric polymorphism to languages that combine static and dynamic typing. We present a system that permits a value of dynamic type to be cast to a polymorphic type and vice versa, with relational parametricity enforced by a kind of dynamic sealing along the lines proposed by Matthews and Ahmed (2008) and Neis, Dreyer, and Rossberg (2009). Our system includes a notion of blame, which allows us to show that when casting between a more-precise type and a less-precise type, any cast failures are due to the less-precisely-typed portion of the program. We also show that a cast from a subtype to its supertype cannot fail.

Supplementary Material

MP4 File (18-mpeg-4.mp4)

Download
472.64 MB

References

[1]

Martin Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13 (2): 237--268, April 1991.

Digital Library

[2]

Amal Ahmed, Jacob Matthews, Robert Bruce Findler, and Philip Wadler. Blame for all. In Workshop on Script-to-Program Evolution (STOP), pages 1--13, 2009.

Digital Library

[3]

Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In ACM International Conference on Functional Programming (ICFP), pages 48--59, October 2002.

Digital Library

[4]

Andrew Gill, John Launchbury, and Simon L. Peyton Jones. A short cut to deforestation. In ACM Conference on Functional Programming Languages and Computer Architecture (FPCA), pages 223--232, September 1993.

Digital Library

[5]

Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop (Scheme), pages 93--104, September 2006.

[6]

Dan Grossman, Greg Morrisett, and Steve Zdancewic. Syntactic type abstraction. ACM Transactions on Programming Languages and Systems, 22 (6): 1037--1080, November 2000.

Digital Library

[7]

Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. Relationally-parametric polymorphic contracts. In Dynamic Languages Symposium (DLS), pages 29--40, 2007.

Digital Library

[8]

Robert Harper. Practical Foundations for Programming Languages. 2007. Working Draft.

[9]

Fritz Henglein. Dynamic typing: Syntax and proof theory. Science of Computer Programming, 22 (3): 197--230, 1994.

Digital Library

[10]

Jacob Matthews and Amal Ahmed. Parametric polymorphism through run-time sealing. In European Symposium on Programming (ESOP), pages 16--31, 2008.

Digital Library

[11]

Jacob Matthews and Robert Bruce Findler. Operational semantics for multi-language programs. In ACM Symposium on Principles of Programming Languages (POPL), pages 3--10, January 2007.

Digital Library

[12]

James H. Morris, Jr. Types are not sets. In ACM Symposium on Principles of Programming Languages (POPL), pages 120--124, October 1973.

Digital Library

[13]

Georg Neis, Derek Dreyer, and Andreas Rossberg. Non-parametric parametricity. In ACM International Conference on Functional Programming (ICFP), pages 135--148, September 2009.

Digital Library

[14]

Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. Dynamic typing with dependent types. In IFIP International Conference on Theoretical Computer Science, pages 437--450, August 2004.

[15]

Benjamin Pierce and Eijiro Sumii. Relating cryptography and polymorphism. Manuscript, 2000. URL www.cis.upenn.edu/ bcpierce/papers/infohide.ps.

[16]

John Reynolds. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing, pages 513--523. North-Holland, 1983.

[17]

Andreas Rossberg. Generativity and dynamic opacity for abstract types. In ACM Conference on Principles and Practice of Declarative Programming (PPDP), pages 241--252, 2003.

Digital Library

[18]

Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop (Scheme), pages 81--92, September 2006.

[19]

Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. System F with type equality coercions. In ACM Workshop on Types in Languages Design and Implementation (TLDI), pages 53--66, 2007.

Digital Library

[20]

Satish Thatte. Type inference with partial types. In International Colloquium on Automata, Languages and Programming (ICALP), volume 317 of phLecture Notes in Computer Science, pages 615--629. Springer-Verlag, 1988.

Digital Library

[21]

Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: From scripts to programs. In Dynamic Languages Symposium (DLS), pages 964--974, October 2006.

Digital Library

[22]

Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In European Symposium on Programming (ESOP), pages 1--16, March 2009.

Digital Library

[23]

Andrew K. Wright. Simple imperative polymorphism. Higher-Order and Symbolic Computation, 8 (4): 343--355, Dec. 1995.

Digital Library

[24]

Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, and Jan Vitek. Integrating typed and untyped code in a scripting language. In ACM Symposium on Principles of Programming Languages (POPL), pages 377--388, 2010.

Digital Library

Cited By

Ye WOliveira BToro M(2024)Merging Gradual TypingProceedings of the ACM on Programming Languages10.1145/36897348:OOPSLA2(648-676)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689734
Igarashi AOzaki SSekiyama TTanabe Y(2024)Space-Efficient Polymorphic Gradual Typing, Mostly ParametricProceedings of the ACM on Programming Languages10.1145/36564418:PLDI(1585-1608)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656441
Gierczak OMenon LDimoulas CAhmed A(2024)Gradually Typed Languages Should Be Vigilant!Proceedings of the ACM on Programming Languages10.1145/36498428:OOPSLA1(864-892)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649842
Show More Cited By

Index Terms

Blame for all
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Procedures, functions and subroutines

Recommendations

Blame for all
POPL '11

Several programming languages are beginning to integrate static and dynamic typing, including Racket (formerly PLT Scheme), Perl 6, and C# 4.0 and the research languages Sage (Gronski, Knowles, Tomb, Freund, and Flanagan, 2006) and Thorn (Wrigstad, ...
Threesomes, with and without blame
POPL '10

How to integrate static and dynamic types? Recent work focuses on casts to mediate between the two. However, adding casts may degrade tail calls into a non-tail calls, increasing space consumption from constant to linear in the depth of calls.

We ...
Threesomes, with and without blame
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

How to integrate static and dynamic types? Recent work focuses on casts to mediate between the two. However, adding casts may degrade tail calls into a non-tail calls, increasing space consumption from constant to linear in the depth of calls.

We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2011

652 pages

ISBN:9781450304900

DOI:10.1145/1926385

General Chair:
Thomas Ball
Microsoft Research, USA
,
Program Chair:
Mooly Sagiv
Tel Aviv University, Israel

ACM SIGPLAN Notices Volume 46, Issue 1
POPL '11
January 2011
624 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1925844
Issue’s Table of Contents

Copyright © 2011 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 ACM 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

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '11

Sponsor:

SIGPLAN

POPL '11: The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 26 - 28, 2011

Texas, Austin, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

98
Total Citations
View Citations
1,077
Total Downloads

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

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ye WOliveira BToro M(2024)Merging Gradual TypingProceedings of the ACM on Programming Languages10.1145/36897348:OOPSLA2(648-676)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689734
Igarashi AOzaki SSekiyama TTanabe Y(2024)Space-Efficient Polymorphic Gradual Typing, Mostly ParametricProceedings of the ACM on Programming Languages10.1145/36564418:PLDI(1585-1608)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656441
Gierczak OMenon LDimoulas CAhmed A(2024)Gradually Typed Languages Should Be Vigilant!Proceedings of the ACM on Programming Languages10.1145/36498428:OOPSLA1(864-892)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649842
YE WOLIVEIRA B(2024)Type-directed operational semantics for gradual typingJournal of Functional Programming10.1017/S095679682400007834Online publication date: 26-Sep-2024
https://doi.org/10.1017/S0956796824000078
SU CCHEN LYANHUI LZHOU Y(2024)Static Blame for gradual typingJournal of Functional Programming10.1017/S095679682400002934Online publication date: 25-Mar-2024
https://doi.org/10.1017/S0956796824000029
Greenman BDimoulas CFelleisen M(2023)Typed–Untyped Interactions: A Comparative AnalysisACM Transactions on Programming Languages and Systems10.1145/357983345:1(1-54)Online publication date: 5-Mar-2023
https://dl.acm.org/doi/10.1145/3579833
Ye WOliveira B(2023)Pragmatic Gradual Polymorphism with ReferencesProgramming Languages and Systems10.1007/978-3-031-30044-8_6(140-167)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_6
Labrada EToro MTanter É(2022)Gradual System FJournal of the ACM10.1145/355598669:5(1-78)Online publication date: 28-Oct-2022
https://dl.acm.org/doi/10.1145/3555986
Ângelo PFlorido M(2022)A Typed Lambda Calculus with Gradual Intersection TypesProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551382(1-13)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1145/3551357.3551382
Devriese DPatrignani MPiessens F(2022)Two Parametricities Versus Three Universal TypesACM Transactions on Programming Languages and Systems10.1145/353965744:4(1-43)Online publication date: 21-Sep-2022
https://dl.acm.org/doi/10.1145/3539657
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