More Like this

1. Casts and costs: harmonizing safety and performance in gradual typing

   https://doi.org/10.1145/3236793  

   Campora, John_Peter; Chen, Sheng; Walkingshaw, Eric (July 2018, Proceedings of the ACM on Programming Languages)

   Gradual typing allows programmers to use both static and dynamic typing in a single program. However, a well-known problem with sound gradual typing is that the interactions between static and dynamic code can cause significant performance degradation. These performance pitfalls are hard to predict and resolve, and discourage users from using gradual typing features. For example, when migrating to a more statically typed program, often adding a type annotation will trigger a slowdown that can be resolved by adding more annotations elsewhere, but since it is not clear where the additional annotations must be added, the easier solution is to simply remove the annotation. To address these problems, we develop: (1) a static cost semantics that accurately predicts the overhead of static-dynamic interactions in a gradually typed program, (2) a technique for efficiently inferring such costs for all combinations of inferrable type assignments in a program, and (3) a method for translating the results of this analysis into specific recommendations and explanations that can help programmers understand, debug, and optimize the performance of gradually typed programs. We have implemented our approach in Herder, a tool for statically analyzing the performance of different typing configurations for Reticulated Python programs. An evaluation on 15 Python programs shows that Herder can use this analysis to accurately and efficiently recommend type assignments that optimize the performance of these programs without sacrificing the safety guarantees provided by static typing. 

   more » « less
2. Putting Gradual Types to Work

   https://doi.org/10.1007/978-3-030-67438-0_4  

   Shivkumar, Bhargav; Naudon, Enrique; Ziarek, Lukasz (January 2021, Practical Aspects of Declarative Languages)

   Morales, J.F.; Orchard, D. (Ed.)

   In this paper, we describe our experience incorporating gradual types in a statically typed functional language with Hindley-Milner style type inference. Where most gradually typed systems aim to improve static checking in a dynamically typed language, we approach it from the opposite perspective and promote dynamic checking in a statically typed language. Our approach provides a glimpse into how languages like SML and OCaml might handle gradual typing. We discuss our implementation and challenges faced—specifically how gradual typing rules apply to our representation of composite and recursive types. We review the various implementations that add dynamic typing to a statically typed language in order to highlight the different ways of mixing static and dynamic typing and examine possible inspirations while maintaining the gradual nature of our type system. This paper also discusses our motivation for adding gradual types to our language, and the practical benefits of doing so in our industrial setting. 

   more » « less
3. Corpse reviver: sound and efficient gradual typing via contract verification

   https://doi.org/10.1145/3434334  

   Moy, Cameron; Nguyễn, Phúc_C; Tobin-Hochstadt, Sam; Van_Horn, David (January 2021, Proceedings of the ACM on Programming Languages)

   Gradually typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks at the boundaries between typed and untyped code. Unfortunately, performance studies have shown that the overhead of these checks can be disastrously high, calling into question the viability of sound gradual typing. In this paper, we show that by building on existing work on soft contract verification, we can reduce or eliminate this overhead. Our key insight is that while untyped code cannot be trusted by a gradual type system, there is no need to consider only the worst case when optimizing a gradually typed program. Instead, we statically analyze the untyped portions of a gradually typed program to prove that almost all of the dynamic checks implied by gradual type boundaries cannot fail, and can be eliminated at compile time. Our analysis is modular, and can be applied to any portion of a program. We evaluate this approach on a dozen existing gradually typed programs previously shown to have prohibitive performance overhead—with a median overhead of 2.5× and up to 80.6× in the worst case—and eliminate all overhead in most cases, suffering only 1.5× overhead in the worst case. 

   more » « less
4. Type-Based Gradual Typing Performance Optimization

   https://doi.org/10.1145/3632931  

   Campora, John_Peter; Khan, Mohammad_Wahiduzzaman; Chen, Sheng (January 2024, Proceedings of the ACM on Programming Languages)

   Gradual typing has emerged as a popular design point in programming languages, attracting significant interests from both academia and industry. Programmers in gradually typed languages are free to utilize static and dynamic typing as needed. To make such languages sound, runtime checks mediate the boundary of typed and untyped code. Unfortunately, such checks can incur significant runtime overhead on programs that heavily mix static and dynamic typing. To combat this overhead without necessitating changes to the underlying implementations of languages, we presentdiscriminative typing. Discriminative typing works by optimistically inferring types for functions and implementing an optimized version of the function based on this type. To preserve safety it also implements an un-optimized version of the function based purely on the provided annotations. With two versions of each function in hand, discriminative typing translates programs so that the optimized functions are called as frequently as possible while also preserving program behaviors. We have implemented discriminative typing in Reticulated Python and have evaluated its performance compared to guarded Reticulated Python. Our results show that discriminative typing improves the performance across 95% of tested programs, when compared to Reticulated, and achieves more than 4× speedup in more than 56% of these programs. We also compare its performance against a previous optimization approach and find that discriminative typing improved performance across 93% of tested programs, with 30% of these programs receiving speedups between 4 to 25 times. Finally, our evaluation shows that discriminative typing remarkably reduces the overhead of gradual typing on many mixed type configurations of programs. In addition, we have implemented discriminative typing in Grift and evaluated its performance. Our evaluation demonstrations that DT significantly improves performance of Grift. 

   more » « less
5. Gradual Typing Performance, Micro Configurations and Macro Perspectives

   Khan, MW; Chen, S (July 2024, Springer, Cham)

   Chin, WN; Xu, Z (Ed.)

   Static typing and dynamic typing have respective strengths and weaknesses, and a language often commits to one typing discipline and inherits the qualities, good or bad. Gradual typing has been developed to reconcile these typing disciplines, allowing a single program to mix both static and dynamic typing. It protects soundness of typed regions with runtime checks when values flown into them do not have required static types. One issue with gradual typing is that such checks can incur significant performance overhead. Previous work on performance has focused on coarse-grained gradual typing where each module (file) has to be fully typed or untyped. In contrast, the performance of fine-grained gradual typing where each single parameter can be partially-typed (such as specifying the parameter as a list without giving element type) has not been investigated. Motivated by this situation, this paper systematically investigates performance of fine-grained gradual typing by studying the performance of more than 1 million programs. These programs are drawn from seven commonly-used benchmarks with different types for parameters: some parameters are untyped, some are statically typed, and others are partially statically typed. The paper observes many interesting phenomena that were previously unknown to the research community. They provide insights into future research directions of understanding, predicting, and optimizing gradual typing performance as well as migrating gradual programs towards more static 

   more » « less