Graph IRs for Impure Higher-Order Languages (Technical Report)

Abstract

This is a companion report for the OOPSLA 2023 paper of the same title, presenting a detailed end-to-end account of the ${\lambda }_{\mathsf{G}}^{\ast }$ graph IR, at a level of detail beyond a regular conference paper. Our first concern is adequacy and soundness of ${\lambda }_{\mathsf{G}}^{\ast }$, which we derive from a direct-style imperative functional language (a variant of Bao et al.'s ${\lambda }^{\ast }$-calculus with reachability types and a simple effect system) by a series of type-preserving translations into a calculus in monadic normalform (MNF). Static reachability types and effects entirely inform ${\lambda }_{\mathsf{G}}^{\ast }$'s dependency synthesis. We argue for its adequacy by proving its functional properties along with dependency safety via progress and preservation lemmas with respect to a notion of call-by-value (CBV) reduction that checks the observed order of effects. Our second concern is establishing the correctness of ${\lambda }_{\mathsf{G}}^{\ast }$'s equational rules that drive compiler optimizations (e.g., DCE, $\lambda$-hoisting, etc.), by proving contextual equivalence using logical relations. A key insight is that the functional properties of dependency synthesis permit a logical relation on ${\lambda }_{\mathsf{G}}^{\ast }$ in MNF in terms of previously developed logical relations for the direct-style ${\lambda }^{\ast }$-calculus. Finally, we also include a longer version of the conference paper's section on code generation and code motion for ${\lambda }_{\mathsf{G}}^{\ast }$ as implemented in Scala~LMS.

arXiv admin note: text overlap with arXiv:2309.05885