A reflection on call-by-value

One way to model a sound and complete translation from a source calculus into a target calculus is with an adjoint or a Galois connection. In the special case of a reflection, one also has that the target calculus is isomorphic to a subset of the source. We show that three widely studied translations form reflections. We use as our source language Moggi's computational lambda calculus, which is an extension of Plotkin's call-by-value calculus. We show that Plotkin's CPS translation, Moggi's monad translation, and Girard's translation to linear logic can all be regarded as reflections form this source language, and we put forward the computational lambda calculus as a model of call-by-value computation that improves on the traditional call-by-value calculus. Our work strengthens Plotkin's and Moggi's original results and improves on recent work based on equational correspondence, which uses equations rather than reductions.