Cited By
View all- 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
How to Evaluate Blame for Gradual Types, Part 2
Article No.: 194, Pages 159 - 186
Abstract
Equipping an existing programming language with a gradual type system requires two major steps. The first and most visible one in academia is to add a notation for types and a type checking apparatus. The second, highly practical one is to provide a type veneer for the large number of existing untyped libraries; doing so enables typed components to import pieces of functionality and get their uses type-checked, without any changes to the libraries. When programmers create such typed veneers for libraries, they make mistakes that persist and cause trouble. The question is whether the academically investigated run-time checks for gradual type systems assist programmers with debugging such mistakes. This paper provides a first, surprising answer to this question via a rational-programmer investigation: run-time checks alone are typically less helpful than the safety checks of the underlying language. Combining Natural run-time checks with blame, however, provides significantly superior debugging hints.
References
[1]
Brett A. Becker, Graham Glanville, Ricardo Iwashima, Claire McDonnell, Kyle Goslin, and Catherine Mooney. 2016. Effective Compiler Error Message Enhancement for Novice Programming Students. Computer Science Education, 26, 2-3 (2016), 148–175. https://doi.org/10.1080/08993408.2016.1225464
[2]
Neil C. C. Brown, Amjad AlTadmri, Sue Sentance, and Michael Kölling. 2018. Blackbox, Five Years On: An Evaluation of a Large-scale Programming Data Collection Project. In ICER. 196–204. https://doi.org/10.1145/3230977.3230991
[3]
John Peter Campora and Sheng Chen. 2020. Taming Type Annotations in Gradual Typing. PACMPL, 4, OOPSLA, 191:1–191:30. https://doi.org/10.1145/3428259
[4]
John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw. 2017. Migrating Gradual Types. PACMPL, 2, POPL (2017), 15:1–15:29. https://doi.org/10.1145/3158103
[5]
Sheng Chen and Martin Erwig. 2014. Counter-Factual Typing for Debugging Type Errors. In POPL. 583–594. https://doi.org/10.1145/2535838.2535863
[6]
Michael Coblenz, Jonathan Aldrich, Brad A. Myers, and Joshua Sunshine. 2020. Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian. PACMPL, 4, OOPSLA (2020), 132:1–132:28. https://doi.org/10.1145/3428200
[7]
Michael Coblenz, Gauri Kambhatla, Paulette Koronkevich, Jenna L. Wise, Celeste Barnaby, Joshua Sunshine, Jonathan Aldrich, and Brad A. Myers. 2021. PLIERS: A Process That Integrates User-Centered Methods into Programming Language Design. ACM Trans. Comput.-Hum. Interact., Article 28, 53 pages. issn:1073-0516 https://doi.org/10.1145/3452379
[8]
Fernando Cristiani and Peter Thiemann. 2021. Generation of TypeScript Declaration Files from JavaScript Code. In International Conference on Managed Programming Languages and Runtimes. 97–112. https://doi.org/10.1145/3475738.3480941
[9]
Richard A. DeMillo, Richard J. Lipton, and Frederick G. Sayward. 1978. Hints on Test Data Selection: Help for the Practicing Programmer. Computer, 11, 4 (1978), 34–41. https://doi.org/10.1109/C-M.1978.218136
[10]
Paul Denny, James Prather, Brett A. Becker, Catherine Mooney, John Homer, Zachary C. Albrecht, and Garrett B. Powell. 2021. On Designing Programming Error Messages for Novices: Readability and its Constituent Factors. In CHI. 55:1–55:15. https://doi.org/10.1145/3411764.3445696
[11]
Benedict du Boulay and Ian Matthew. 1984. Fatal Error in Pass Zero: How not to Confuse Novices. In Readings on Cognitive Ergonomics - Mind and Computers. 178, 132–141. https://doi.org/10.1007/3-540-13394-1_11
[12]
Asger Feldthaus and Anders Møller. 2014. Checking Correctness of TypeScript Interfaces for JavaScript Libraries. In OOPSLA. 1–16. https://doi.org/10.1145/2660193.2660215
[13]
Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for Higher-Order Functions. In ICFP. 48–59. https://doi.org/10.1145/581478.581484
[14]
Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. 1998. Classes and Mixins. In POPL. 171–183. https://doi.org/10.1145/268946.268961
[15]
Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs. In POPL. 303–315. https://doi.org/10.1145/2676726.2676992
[16]
Ben Greenman. 2020. Deep and Shallow Types. Ph. D. Dissertation. Northeastern University.
[17]
Ben Greenman, Matthias Felleisen, and Christos Dimoulas. 2019. Complete Monitors for Gradual Types. PACMPL, 3, OOPSLA (2019), 122:1–122:29. https://doi.org/10.1145/3360548
[18]
Ben Greenman, Lukas Lazarek, Christos Dimoulas, and Matthias Felleisen. 2022. A Transient Semantics for Typed Racket. Programming, 2, 6, https://doi.org/10.22152/programming-journal.org/2022/6/9
[19]
Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, Robert Bruce Findler, Jan Vitek, and Matthias Felleisen. 2019. How to Evaluate the Performance of Gradual Type Systems. JFP, 29, e4 (2019), 1–45. https://doi.org/10.1017/S0956796818000217
[20]
Stefan Hanenberg. 2010. An Experiment about Static and Dynamic Type Systems: Doubts about the Positive Impact of Static Type Systems on Development Time. In OOPSLA. 22–35. https://doi.org/10.1145/1869459.1869462
[21]
Stefan Hanenberg, Sebastian Kleinschmager, Romain Robbes, Éric Tanter, and Andreas Stefik. 2014. An empirical study on the impact of static typing on software maintainability. Empirical Software Engineering, 19, 5 (2014), 1335–1382. https://doi.org/10.1007/s10664-013-9289-1
[22]
Joseph Henrich, Robert Boyd, Samuel Bowles, Colin Camerer, Ernst Fehr, Herbert Gintis, and Richard McElreath. 2001. In Search of Homo Economicus: Behavioral Experiments in 15 Small-Scale Societies. American Economic Review, 91, 2 (2001), 73–78. https://doi.org/10.1257/aer.91.2.73
[23]
Joshua Hoeflich, Robert Bruce Findler, and Manuel Serrano. 2022. Highly Illogical, Kirk: Spotting Type Mismatches in the Large despite Broken Contracts, Unsound Types, and Too Many Linters. PACMPL, 6, OOPSLA (2022), 142:1–142:26. https://doi.org/10.1145/3563305
[24]
Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 2001. Featherweight Java: A Minimal Core Calculus for Java and GJ. TOPLAS, 23, 3 (2001), 396–450. https://doi.org/10.1145/503502.503505
[25]
Ralph Keller and Urs Hölzle. 1998. Binary component adaptation. In ECOOP. 307–329. https://doi.org/10.1007/BFb0054097
[26]
Erik Krogh Kristensen and Anders Møller. 2017. Inference and Evolution of TypeScript Declaration Files. In FASE. 99–115. https://doi.org/10.1007/978-3-662-54494-5_6
[27]
Erik Krogh Kristensen and Anders Møller. 2017. Type Test Scripts for TypeScript Testing. PACMPL, 1, OOPSLA (2017), 90:1–90:25. https://doi.org/10.1145/3133914
[28]
Lukas Lazarek, Ben Greenman, Matthias Felleisen, and Christos Dimoulas. 2021. How to Evaluate Blame for Gradual Types. PACMPL, 5, ICFP (2021), 68:1–68:29. https://doi.org/10.1145/3473573
[29]
Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert B. Findler, and Christos Dimoulas. 2020. Does Blame Shifting Work? PACMPL, 4, POPL (2020), 65:1–65:29. https://doi.org/10.1145/3373113
[30]
Richard J Lipton. 1971. Fault Diagnosis of Computer Programs. Carnegie Mellon University, Pittsburgh, PA.
[31]
Justin Lubin and Sarah E. Chasins. 2021. How Statically-Typed Functional Programmers Write Code. PACMPL, 5, OOPSLA (2021), 155:1–155:30. https://doi.org/10.1145/3485532
[32]
Kai-Uwe Mätzel and Peter Schnorf. 1997. Dynamic component adaptation. Ubilab Technical Report 97.6.
[33]
Microsoft. [n. d.]. TypeScript. Retrieved February 23, 2023 from https://www.typescriptlang.org
[34]
Zeina Migeed and Jens Palsberg. 2019. What is Decidable about Gradual Types? PACMPL, 4, POPL (2019), 29:1–29:29 pages. https://doi.org/10.1145/3371097
[35]
John Stuart Mill. 1874. Essays on Some Unsettled Questions of Political Economy. Longmans, Green, Reader, and Dyer.
[36]
Robin Milner, Robert Harper, David MacQueen, and Mads Tofte. 1998. The Definition of Standard ML, Revised Edition. MIT Press.
[37]
Robin Milner, Mads Tofte, and Robert Harper. 1990. The Definition of Standard ML. MIT Press.
[38]
Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi. 2019. Dynamic Type Inference for Gradual Hindley–Milner Typing. PACMPL, 3, POPL (2019), 18:1–18:29 pages. https://doi.org/10.1145/3290331
[39]
Todd Mytkowicz, Amer Diwan, Matthias Hauswirth, and Peter F. Sweeney. 2009. Producing Wrong Data without Doing Anything Obviously Wrong!. In ASPLOS. 265–276. isbn:9781605584065 https://doi.org/10.1145/1508244.1508275
[40]
Zvonimir Pavlinovic, Tim King, and Thomas Wies. 2014. Finding Minimum Type Error Sources. In OOPSLA. 525–542. https://doi.org/10.1145/2660193.2660230
[41]
Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, and Arjun Guha. 2021. Solver-Based Gradual Type Migration. PACMPL, 5, OOPSLA (2021), 111:1–111:27 pages. https://doi.org/10.1145/3485488
[42]
Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. 2012. The Ins and Outs of Gradual Type Inference. In POPL. 481–494. https://doi.org/10.1145/2103656.2103714
[43]
Eric L. Seidel, Ranjit Jhala, and Westley Weimer. 2016. Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong). In ICFP. 228–242. https://doi.org/10.1145/2951913.2951915
[44]
Eric L. Seidel, Ranjit Jhala, and Westley Weimer. 2018. Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong). 28 (2018), e13. https://doi.org/10.1017/S0956796818000126
[45]
Herbert A. Simon. 1947. Administrative Behavior. MacMillan.
[46]
Samuel Spiza and Stefan Hanenberg. 2014. Type Names without Static Type Checking Already Improve the Usability of APIs (as Long as the Type Names Are Correct): An Empirical Study. In Modularity. 99–108. https://doi.org/10.1145/2577080.2577098
[47]
Vincent St-Amour and Neil Toronto. 2013. Experience Report: Applying Random Testing to a Base Type Environment. In ICFP. 351–356. https://doi.org/10.1145/2500365.2500616
[48]
T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. 2012. Chaperones and Impersonators: Run-time Support for Reasonable Interposition. In OOPSLA. 943–962. https://doi.org/10.1145/2384616.2384685
[49]
Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. 2016. Is Sound Gradual Typing Dead? In POPL. 456–468. https://doi.org/10.1145/2837614.2837630
[50]
Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage Migration: from Scripts to Programs. In DLS. 964–974. https://doi.org/10.1145/1176617.1176755
[51]
Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme. In POPL. 395–406. https://doi.org/10.1145/1328438.1328486
[52]
Sam Tobin-Hochstadt and Matthias Felleisen. 2010. Logical Types for Untyped Languages. In ICFP. 117–128. https://doi.org/10.1145/1863543.1863561
[53]
Sam Tobin-Hochstadt, Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. 2017. Migratory Typing: Ten Years Later. In SNAPL. 17:1–17:17. https://doi.org/10.4230/LIPIcs.SNAPL.2017.17
[54]
Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi. 2018. The Behavior of Gradual Types: a User Study. In DLS. 1–12. https://doi.org/10.1145/3276945.3276947
[55]
Michael M. Vitousek, Andrew Kent, Jeremy G. Siek, and Jim Baker. 2014. Design and Evaluation of Gradual Typing for Python. In DLS. 45–56. https://doi.org/10.1145/2661088.2661101
[56]
Michael M. Vitousek, Jeremy G. Siek, and Avik Chaudhuri. 2019. Optimizing and Evaluating Transient Gradual Typing. In DLS. 28–41. https://doi.org/10.1145/3359619.3359742
[57]
Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. 2017. Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems. In POPL. 762–774. https://doi.org/10.1145/3009837.3009849
[58]
Philip Wadler and Robert Bruce Findler. 2009. Well-typed Programs Can’t Be Blamed. In ESOP. 1–15. https://doi.org/10.1007/978-3-642-00590-9_1
[59]
Richard L. Wexelblat. 1976. Maxims for Malfeasant Designers, or How to Design Languages to Make Programming as Difficult as Possible. In ICSE. 331–336. https://doi.org/10.5555/800253.807695
[60]
Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. 2017. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript. In ECOOP. 28 pages. https://doi.org/10.4230/LIPIcs.ECOOP.2017.28
[61]
Baijun Wu and Sheng Chen. 2017. How Type Errors Were Fixed and What Students Did? PACMPL, 1, OOPSLA (2017), 105:1–105:27 pages. https://doi.org/10.1145/3133929
[62]
Danfeng Zhang and Andrew C. Myers. 2014. Toward General Diagnosis of Static Errors. In POPL. 569–581. https://doi.org/10.1145/2535838.2535870
Index Terms
- How to Evaluate Blame for Gradual Types, Part 2
Recommendations
Gradual typing with union and intersection types
We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...
How to evaluate blame for gradual types
Programming language theoreticians develop blame assignment systems and prove blame theorems for gradually typed programming languages. Practical implementations of gradual typing almost completely ignore the idea of blame assignment. This contrast ...
A Typed Lambda Calculus with Gradual Intersection Types
PPDP '22: Proceedings of the 24th International Symposium on Principles and Practice of Declarative ProgrammingIntersection types have the power to type expressions which are all of many different types. Gradual types combine type checking at both compile-time and run-time. Here we combine these two approaches in a new typed calculus that harness both of their ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2023
981 pages
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 31 August 2023
Published in PACMPL Volume 7, Issue ICFP
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 314Total Downloads
- Downloads (Last 12 months)214
- Downloads (Last 6 weeks)27
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
Cited By
View all- 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
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.
Sign in