TY - JOUR
T1 - A Transient Semantics for Typed Racket
AU - Greenman, Ben
AU - Lazarek, Lukas
AU - Dimoulas, Christos
AU - Felleisen, Matthias
N1 - Funding Information:
Acknowledgements Felleisen and Greenman were partly supported by NSF grant SHF 1763922. Greenman also received support from NSF grant 2030859 to the CRA for the CIFellows project. Thanks to Robby Findler and Northwestern PLT for their valuable feedback at various stages of this work. This paper was supported in part by the NSF grant CNS-1823244.
Publisher Copyright:
© Ben Greenman, Lukas Lazarek, Christos Dimoulas, and Matthias Felleisen.
PY - 2022
Y1 - 2022
N2 - 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. Fur-thermore, 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. Reticu-lated 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.
AB - 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. Fur-thermore, 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. Reticu-lated 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.
KW - compilers
KW - gradual typing
KW - migratory typing
KW - transient semantics
UR - http://www.scopus.com/inward/record.url?scp=85128171878&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85128171878&partnerID=8YFLogxK
U2 - 10.22152/programming-journal.org/2022/6/9
DO - 10.22152/programming-journal.org/2022/6/9
M3 - Article
AN - SCOPUS:85128171878
SN - 2473-7321
VL - 6
JO - Art, Science, and Engineering of Programming
JF - Art, Science, and Engineering of Programming
IS - 2
M1 - 9
ER -