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 present discriminative typ ing. 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 perfor- mance 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.
Fri 19 JanDisplayed time zone: London change
16:50 - 18:10 | Gradual Typing and VerificationPOPL at Kelvin Lecture Chair(s): Ronald Garcia University of British Columbia | ||
16:50 20mTalk | Securing Verified IO Programs Against Unverified Code in F* POPL Cezar-Constantin Andrici MPI-SP, Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Cătălin Hriţcu MPI-SP, Guido Martínez Microsoft Research, Exequiel Rivas Tallinn University of Technology, Éric Tanter University of Chile, Théo Winterhalter INRIA Saclay Pre-print | ||
17:10 20mTalk | Sound Gradual Verification with Symbolic Execution POPL Conrad Zimmerman Brown University, Jenna DiVincenzo (Wise) Purdue University, Jonathan Aldrich Carnegie Mellon University | ||
17:30 20mTalk | Type-based Gradual Typing Performance Optimization POPL | ||
17:50 20mTalk | Total Type Error Localization and Recovery with HolesDistinguished Paper POPL Eric Zhao University of Michigan, Raef Maroof University of Michigan, Anand Dukkipati University of Michigan, Andrew Blinn University of Michigan, Zhiyi Pan University of Michigan, Cyrus Omar University of Michigan |