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/
Go to the corresponding LIPIcs Volume Portal

Tsuda, Yuya ; Igarashi, Atsushi ; Tabuchi, Tomoya

Space-Efficient Gradual Typing in Coercion-Passing Style

pdf-format:
LIPIcs-ECOOP-2020-8.pdf (0.7 MB)

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI