Call-By-Name Is Just Call-By-Value with Delimited Control

TL;DR

This paper introduces a lambda calculus extended with delimited control operators, demonstrating it can express both lambda calculus and effects, bridging call-by-name and call-by-value paradigms through a novel reduction theory.

Contribution

It presents a new lambda calculus with shift0 and control delimiter, showing it can embed lambda calculus with beta and eta reductions and unify various calculi.

Findings

Delimited control operators can express lambda calculus and effects

The calculus $\Lambda_\$ $ can embed lambda calculus with beta and eta reductions

Call-by-name can simulate call-by-value with delimited control

Abstract

Delimited control operator shift0 exhibits versatile capabilities: it can express layered monadic effects, or equivalently, algebraic effects. Little did we know it can express lambda calculus too! We present $ \Lambda_\$ $, a call-by-value lambda calculus extended with shift0 and control delimiter $ \$ $ with carefully crafted reduction theory, such that the lambda calculus with beta and eta reductions can be isomorphically embedded into $ \Lambda_\$ $ via a right inverse of a continuation-passing style translation. While call-by-name reductions of lambda calculus can trivially simulate its call-by-value version, we show that addition of shift0 and $ \$ $ is the golden mean of expressive power that suffices to simulate beta and eta reductions while still admitting a simulation back. As a corollary, calculi $ \Lambda\mu_v $, $ \lambda_\$ $, $ \Lambda_\$ $ and $ \lambda $ all correspond equationally.