Galois connecting call-by-value and call-by-name
Dylan McDermott, Alan Mycroft
TL;DR
This work develops a general framework to relate call-by-value and call-by-name evaluation in languages with effects by leveraging Levy's call-by-push-value (CBPV) as a unifying framework. It first introduces a denotational relation between the two CBPV translations $V\llparenthesis e \rrparenthesis$ and $N\llparenthesis e \rrparenthesis$ within order-enriched models, identifying effect-conditions that permit discarding, duplicating, and reordering effects. It then constructs Galois connections between the call-by-value and call-by-name interpretations of types, yielding a model-agnostic reasoning principle: for any term $e$ of type $\tau$, $\mathcal{V}\llbracket e \rrbracket \preccurlyeq_{ctx} \Psi_{\tau}(\mathcal{N}\llbracket e \rrbracket [\hat{\Phi}_{\Gamma}])$. The principle is applied to examples including no effects, divergence, and nondeterminism, showing that termination under value implies termination with the same result under name, and that nondeterministic results extend in a monotone way. Overall, the paper provides a principled, semantics-based method to reason about evaluation-order changes and to identify which computational effects admit a precise correspondence between the two semantics.
Abstract
We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with computational effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving properties like these. The key ingredient is Levy's call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We show that the call-by-value and call-by-name translations of expressions into call-by-push-value have related observable behaviour under certain conditions on computational effects, which we identify. We then use this fact to construct maps between the call-by-value and call-by-name interpretations of types, and identify further properties of effects that imply these maps form a Galois connection. These properties hold for some computational effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example computational effects including divergence and nondeterminism.