What is decidable about gradual types?
By Zeina Migeed, Jens Palsberg. 2019
16 citations recorded by the source corpus.
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.
Subfields: Artificial Intelligence, Hardware and Architecture, Information Systems, Program Analysis & Verification
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
In Hardware and Architecture
In Information Systems
In Program Analysis & Verification
Citations in the corpus
- Do Machine Learning Models Produce TypeScript Types that Type Check? (2023, methodology): “The earliest approach was a variation of unification-based type inference [47], and more recent work uses a wide range of techniques [9, 12, 21, 34, 35, 40].”