B. Greenman, и Z. Migeed. Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, стр. 30--39. ACM, (2018)
DOI: 10.1145/3162066
Аннотация
Gradual typing systems ensure type soundness by transforming static type annotations into run-time checks. These checks provide semantic guarantees, but may come at a large cost in performance. In particular, recent work by Takikawa et al. suggests that enforcing a conventional form of type soundness may slow a program by two orders of magnitude. Since different gradual typing systems satisfy different notions of soundness, the question then arises: what is the cost of such varying notions of soundness? This paper answers an instance of this question by applying Takikawa et al.'s evaluation method to Reticulated Python, which satisfies a notion of type-tag soundness. We find that the cost of soundness in Reticulated is at most one order of magnitude, and increases linearly with the number of type annotations.
%0 Conference Paper
%1 Greenman:2017:CTS
%A Greenman, Ben
%A Migeed, Zeina
%B Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
%D 2018
%I ACM
%K GradualTyping Python Typing
%P 30--39
%R 10.1145/3162066
%T On the Cost of Type-tag Soundness
%X Gradual typing systems ensure type soundness by transforming static type annotations into run-time checks. These checks provide semantic guarantees, but may come at a large cost in performance. In particular, recent work by Takikawa et al. suggests that enforcing a conventional form of type soundness may slow a program by two orders of magnitude. Since different gradual typing systems satisfy different notions of soundness, the question then arises: what is the cost of such varying notions of soundness? This paper answers an instance of this question by applying Takikawa et al.'s evaluation method to Reticulated Python, which satisfies a notion of type-tag soundness. We find that the cost of soundness in Reticulated is at most one order of magnitude, and increases linearly with the number of type annotations.
%@ 978-1-4503-5587-2
@inproceedings{Greenman:2017:CTS,
abstract = {Gradual typing systems ensure type soundness by transforming static type annotations into run-time checks. These checks provide semantic guarantees, but may come at a large cost in performance. In particular, recent work by Takikawa et al. suggests that enforcing a conventional form of type soundness may slow a program by two orders of magnitude. Since different gradual typing systems satisfy different notions of soundness, the question then arises: what is the cost of such varying notions of soundness? This paper answers an instance of this question by applying Takikawa et al.'s evaluation method to Reticulated Python, which satisfies a notion of type-tag soundness. We find that the cost of soundness in Reticulated is at most one order of magnitude, and increases linearly with the number of type annotations.},
acmid = {3162066},
added-at = {2018-07-15T11:25:31.000+0200},
author = {Greenman, Ben and Migeed, Zeina},
biburl = {https://www.bibsonomy.org/bibtex/2436dd0e7406db124ae6d758363936984/gron},
booktitle = {Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation},
description = {On the cost of type-tag soundness},
doi = {10.1145/3162066},
interhash = {6908bef35ca015bb6e09cd28a510971e},
intrahash = {436dd0e7406db124ae6d758363936984},
isbn = {978-1-4503-5587-2},
keywords = {GradualTyping Python Typing},
location = {Los Angeles, CA, USA},
numpages = {10},
pages = {30--39},
publisher = {ACM},
series = {PEPM'18},
timestamp = {2018-07-15T11:25:31.000+0200},
title = {{On the Cost of Type-tag Soundness}},
year = 2018
}