License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2020.8
URN: urn:nbn:de:0030-drops-131658
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13165/
Tsuda, Yuya ;
Igarashi, Atsushi ;
Tabuchi, Tomoya
Space-Efficient Gradual Typing in Coercion-Passing Style
Abstract
Herman et al. pointed out that the insertion of run-time checks into a gradually typed program could hamper tail-call optimization and, as a result, worsen the space complexity of the program. To address the problem, they proposed a space-efficient coercion calculus, which was subsequently improved by Siek et al. The semantics of these calculi involves eager composition of run-time checks expressed by coercions to prevent the size of a term from growing. However, it relies also on a nonstandard reduction rule, which does not seem easy to implement. In fact, no compiler implementation of gradually typed languages fully supports the space-efficient semantics faithfully.
In this paper, we study coercion-passing style, which Herman et al. have already mentioned, as a technique for straightforward space-efficient implementation of gradually typed languages. A program in coercion-passing style passes "the rest of the run-time checks" around - just like continuation-passing style (CPS), in which "the rest of the computation" is passed around - and (unlike CPS) composes coercions eagerly. We give a formal coercion-passing translation from λS by Siek et al. to λS₁, which is a new calculus of first-class coercions tailored for coercion-passing style, and prove correctness of the translation. We also implement our coercion-passing style transformation for the Grift compiler developed by Kuhlenschmidt et al. An experimental result shows stack overflow can be prevented properly at the cost of up to 3 times slower execution for most partially typed practical programs.
BibTeX - Entry
@InProceedings{tsuda_et_al:LIPIcs:2020:13165,
author = {Yuya Tsuda and Atsushi Igarashi and Tomoya Tabuchi},
title = {{Space-Efficient Gradual Typing in Coercion-Passing Style}},
booktitle = {34th European Conference on Object-Oriented Programming (ECOOP 2020)},
pages = {8:1--8:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-154-2},
ISSN = {1868-8969},
year = {2020},
volume = {166},
editor = {Robert Hirschfeld and Tobias Pape},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13165},
URN = {urn:nbn:de:0030-drops-131658},
doi = {10.4230/LIPIcs.ECOOP.2020.8},
annote = {Keywords: Gradual typing, coercion calculus, coercion-passing style, dynamic type checking, tail-call optimization}
}
Keywords: |
|
Gradual typing, coercion calculus, coercion-passing style, dynamic type checking, tail-call optimization |
Collection: |
|
34th European Conference on Object-Oriented Programming (ECOOP 2020) |
Issue Date: |
|
2020 |
Date of publication: |
|
06.11.2020 |