by Mar­ius Müller, Philipp Schus­ter, Jonathan Lin­de­gaard Starup, Klaus Os­ter­mann, and Jonathan Im­manuel Brachthäuser

In Proc. Int’l Conf. Ob­ject-Ori­ented Pro­gram­ming, Sys­tems, Lan­guages and Ap­pli­ca­tions (OOP­SLA). ACM Press, 2023.

This pub­li­ca­tion is re­lated to the Ef­fects re­search pro­ject.

Ab­stract

Ef­fect han­dlers are a high-level ab­strac­tion that en­ables pro­gram­mers to use ef­fects in a struc­tured way. They have gained a lot of pop­u­lar­ity within acad­e­mia and sub­se­quently also in in­dus­try. How­ever, the ab­strac­tion often comes with a sig­nif­i­cant run­time cost and there has been in­ten­sive re­search re­cently on how to re­duce this price. A promis­ing ap­proach in this re­gard is to im­ple­ment ef­fect han­dlers using a CPS trans­la­tion and to pro­vide suf­fi­cient in­for­ma­tion about the nest­ing of han­dlers. With this in­for­ma­tion the CPS trans­la­tion can de­cide how ef­fects have to be lifted through han­dlers, i.e., which han­dlers need to be skipped, in order to han­dle the ef­fect at the cor­rect place. A struc­tured way to make this in­for­ma­tion avail­able is to use a cal­cu­lus with a re­gion sys­tem and ex­plicit sub­re­gion ev­i­dence. Such cal­culi, how­ever, are quite ver­bose, which makes them im­prac­ti­cal to use as a source-level lan­guage. We pre­sent a method to infer the lift­ing in­for­ma­tion for a cal­cu­lus un­der­ly­ing a source-level lan­guage. This cal­cu­lus uses sec­ond-class ca­pa­bil­i­ties for the safe use of ef­fects. To do so, we de­fine a typed trans­la­tion to a cal­cu­lus with re­gions and ev­i­dence and we show that this lift-in­fer­ence trans­la­tion is ty­pa­bil­ity- and se­man­tics-pre­serv­ing. On the one hand, this ex­poses the pre­cise re­la­tion be­tween the sec­ond-class prop­erty and the struc­ture given by re­gions. On the other hand, it closes a gap in a com­piler pipeline en­abling ef­fi­cient com­pi­la­tion of the source-level lan­guage. We have im­ple­mented lift in­fer­ence in this com­piler pipeline and con­ducted bench­marks which in­di­cate that the ap­proach is in­deed work­ing.