Programmers can use gradual types to migrate programs to have more precise type annotations and thereby improve their readability, efficiency, and safety. Such migration requires an exploration of the migration space and can benefit from tool support, as shown in previous work. Our goal is to provide a foundation for better tool support by settling decidability questions about migration with gradual types. We present three algorithms and a hardness result for deciding key properties and we explain how they can be useful during an exploration. In particular, we show how to decide whether the migration space is finite, whether it has a top element, and whether it is a singleton. We also show that deciding whether it has a maximal element is NP-hard. Our implementation of our algorithms worked as expected on a suite of microbenchmarks.
| What is Decidable about Gradual Types? (proceedings-version-with-badges.pdf) | 483KiB |
| (POPL_slides (1).pdf) | 269KiB |
Wed 22 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05 | Gradual Typing / Language DesignResearch Papers at Ile de France III (IDF III) Chair(s): Jeremy G. Siek Indiana University, USA | ||
14:00 21mTalk | What is Decidable about Gradual Types? Research Papers Zeina Migeed University of California, Los Angeles, Jens Palsberg University of California, Los Angeles Link to publication DOI Media Attached File Attached | ||
14:21 21mTalk | Graduality and Parametricity: Together Again for the First Time Research Papers Max S. New Northeastern University, Dustin Jamner Northeastern University, USA, Amal Ahmed Northeastern University, USA Link to publication DOI Media Attached | ||
14:43 21mTalk | Does Blame Shifting Work? Research Papers Lukas Lazarek Northwestern University, Alexis King Northwestern University, Samanvitha Sundar Northwestern University, Robert Bruce Findler Northwestern University, USA, Christos Dimoulas PLT @ Northwestern University Link to publication DOI Media Attached | ||