Write a Blog >>
Sat 25 Jan 2020 14:32 - 15:05 at Orleans - Coercions Chair(s): Jeremy G. Siek

Herman et al. (2007, 2010) 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 Garcia, et al. (2009) and Siek et al. (2015). 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 run-time checks” around—just like continuation-passing style (CPS), in which “the rest of computation” has been passed around—and (unlike CPS) composes coercions eagerly. We give a formal coercion-passing translation from $\lambda$S by Siek et al. to $\lambda$S$_1$, 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. and give a preliminary experimental result.

Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change

14:00 - 15:05: CoercionsWGT at Orleans
Chair(s): Jeremy G. SiekIndiana University, USA
14:00 - 14:32
Hypercoercions and a Framework for Equivalence of Cast Calculi
Kuang-Chen LuIndiana University Bloomington, Jeremy G. SiekIndiana University, USA, Andre KuhlenschmidtIndiana University
14:32 - 15:05
Space-Efficient Gradual Typing in Coercion-Passing Style
Yuya TsudaKyoto University, Atsushi IgarashiKyoto University, Japan, Tomoya TabuchiKyoto University