Mixed-typed languages enable programmers to link typed and untyped components
in various ways. Some offer rich type systems to facilitate the smooth
migration of untyped code to the typed world; others merely provide a
convenient form of type Dynamic together with a conventional structural type
system. Orthogonal to this dimension, Natural systems ensure the integrity of
types with a sophisticated contract system, while Transient systems insert
simple first-order checks at strategic places within typed code. Furthermore,
each method of ensuring type integrity comes with its own blame-assignment
strategy.
Typed Racket has a rich migratory type system and enforces the types with a
Natural semantics. Reticulated Python has a simple structural type system
extended with Dynamic and enforces types with a Transient semantics. While
Typed Racket satisfies the most stringent gradual-type soundness properties at
a significant performance cost, Reticulated Python seems to limit the
performance penalty to a tolerable degree and is nevertheless type sound. This
comparison raises the question of whether Transient checking is applicable to
and beneficial for a rich migratory type system.
This paper reports on the surprising difficulties of adapting the Transient
semantics of Reticulated Python to the rich migratory type system of Typed
Racket. The resulting implementation, Shallow Typed Racket, is faster than the
standard Deep Typed Racket but only when the Transient blame assignment
strategy is disabled. For language designers, this report provides valuable
hints on how to equip an existing compiler to support a Transient semantics.
For theoreticians, the negative experience with Transient blame calls for a
thorough investigation of this strategy.
more »
« less
Gradual Soundness: Lessons from Static Python
Context:
Gradually-typed languages allow typed and untyped code to interoperate, but typically come with significant drawbacks. In some languages, the types are unreliable; in others, communication across type boundaries can be extremely expensive; and still others allow only limited forms of interoperability. The research community is actively seeking a sound, fast, and expressive approach to gradual typing.
Inquiry:
This paper describes Static Python, a language developed by engineers at Instagram that has proven itself sound, fast, and reasonably expressive in production. Static Python’s approach to gradual types is essentially a programmer-tunable combination of the concrete and transient approaches from the literature. Concrete types provide full soundness and low performance overhead, but impose nonlocal constraints. Transient types are sound in a shallow sense and easier to use; they help to bridge the gap between untyped code and typed concrete code.
Approach:
We evaluate the language in its current state and develop a model that captures the essence of its approach to gradual types. We draw upon personal communication, bug reports, and the Static Python regression test suite to develop this model.
Knowledge:
Our main finding is that the gradual soundness that arises from a mix of concrete and transient types is an effective way to lower the maintenance cost of the concrete approach. We also find that method-based JIT technology can eliminate the costs of the transient approach. On a more technical level, this paper describes two contributions: a model of Static Python and a performance evaluation of Static Python. The process of formalization found several errors in the implementation, including fatal errors.
Grounding:
Our model of Static Python is implemented in PLT Redex and tested using property-based soundness tests and 265 tests from the Static Python regression suite. This paper includes a small core of the model to convey the main ideas of the Static Python approach and its soundness. Our performance claims are based on production experience in the Instagram web server. Migrations to Static Python in the server have caused a 3.7\% increase in requests handled per second at maximum CPU load.
Importance:
Static Python is the first sound gradual language whose piece-meal application to a realistic codebase has consistently improved performance. Other language designers may wish to replicate its approach, especially those who currently maintain unsound gradual languages and are seeking a path to soundness.
more »
« less
- Award ID(s):
- 2227863
- PAR ID:
- 10472729
- Publisher / Repository:
- Programming Journal
- Date Published:
- Journal Name:
- The Art, Science, and Engineering of Programming
- Volume:
- 7
- Issue:
- 1
- ISSN:
- 2473-7321
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
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
-
more » « less
In gradual typing, different languages perform different dynamic type checks for the same program even though the languages have the same static type system. This raises the question of whether, given a gradually typed language, the combination of the translation that injects checks in well-typed terms and the dynamic semantics that determines their behavior sufficiently enforce the static type system of the language. Neither type soundness, nor complete monitoring, nor any other meta-theoretic property of gradually typed languages to date provides a satisfying answer.
In response, we present vigilance, a semantic analytical instrument that defines when the check-injecting translation and dynamic semantics of a gradually typed language are adequate for its static type system. Technically, vigilance asks if a given translation-and-semantics combination enforces the complete run-time typing history of a value, which consists of all of the types associated with the value. We show that the standard combination for so-called Natural gradual typing is vigilant for the standard simple type system, but the standard combination for Transient gradual typing is not. At the same time, the standard combination for Transient is vigilant for a tag type system but the standard combination for Natural is not. Hence, we clarify the comparative type-level reasoning power between the two most studied approaches to sound gradual typing. Furthermore, as an exercise that demonstrates how vigilance can guide design, we introduce and examine a new theoretical static gradual type system, dubbed truer, that is stronger than tag typing and more faithfully reflects the type-level reasoning power that the dynamic semantics of Transient gradual typing can guarantee.
-
more » « less
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 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
-
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
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.22152/programming-journal.org/2023/7/2
