Gradual typing integrates static and dynamic typing by introducing a dynamic type and a consistency relation. A problem of gradual type systems is that dynamic types can easily hide erroneous data flows since consistency relations are not transitive. Therefore, a more rigorous static check is required to reveal these hidden data flows statically. However, in order to preserve the expressiveness of gradually typed languages, static checks for gradually typed languages cannot simply reject programs with potentially erroneous data flows. By contrast, a more reasonable request is to show how these data flows can affect the execution of the program. In this paper, we propose and formalize Static Blame, a framework that can reveal hidden data flows for gradually typed programs and establish the correspondence between static-time data flows and runtime behavior. With this correspondence, we build a classification of potential errors detected from hidden data flows and formally characterize the possible impact of potential errors in each category on program execution, without simply rejecting the whole program. We implemented Static Blame on Grift, an academic gradually typed language, and evaluated the effectiveness of Static Blame by mutation analysis to verify our theoretical results. Our findings revealed that Static Blame exhibits a notable level of precision and recall in detecting type-related bugs. Furthermore, we conducted a manual classification to elucidate the reasons behind instances of failure. We also evaluated the performance of Static Blame, showing a quadratic growth in run time as program size increases.
Tue 3 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | Type TheoryICFP Papers and Events / JFP First Papers at Green 1-2-3 Chair(s): Brent Yorgey Hendrix College | ||
13:30 18mTalk | Normalization by evaluation for modal dependent type theoryJFP First Paper JFP First Papers Jason Z.S. Hu McGill University, Junyoung Jang McGill University, Brigitte Pientka McGill University DOI | ||
13:48 18mTalk | Closure-Free Functional Programming in a Two-Level Type Theory ICFP Papers and Events András Kovács University of Gothenburg DOI Pre-print | ||
14:06 18mTalk | Gradual Indexed Inductive Types ICFP Papers and Events Mara Malewski Correa University of Chile, Kenji Maillard Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile DOI | ||
14:24 18mTalk | Dependent Ghosts Have a Reflection for Free ICFP Papers and Events Théo Winterhalter Inria DOI | ||
14:42 18mTalk | Static Blame for gradual typingJFP First Paper JFP First Papers Chenghao Su Nanjing University, Lin Chen Nanjing University, Yanhui Li Nanjing University, Yuming Zhou Nanjing University DOI |