We use as our source language Moggi's computational lambda calculus, which is an extension of Plotkin's call-by-value calculus.
Our source calculus is the computational calculus, [Lambda.sub.c], of Moggi [1988], which extends the call-by-value lambda calculus, [Lambda.sub.v], of Plotkin [1975].
Further, we show for the first time that Moggi's computational lambda calculus [Lambda.sub.c], actually has computational content, and therefore might serve as an improvement over Plotkin's call-by-value lambda calculus [Lambda.sub.v].
Plotkin [1975] showed, among other things, that the call-by-value CPS translation was sound but not complete, in that it preserves but does not reflect equalities.
A baker's dozen of years later, Moggi [1988] showed, among other things, that the call-by-value monad translation is both sound and complete, in that it preserves and reflects equalities.
Let us review the traditional translation from the call-by-value calculus into the monad calculus, and see why it fails to be a reflection.
Plotkin's call-by-value calculus [Lambda.sub.Nu] is summarized in Figure 3.
while if L is not a value then the equivalence does not hold in the call-by-value calculus.
This provides an analogue of Plotkin's indifference property, which states that call-by-value and call-by-name evaluation yield the same result for terms in CPS.
which is not provable in the call-by-value calculus if L is not a value.
[1995] were concerned with a similar problem: finding translations between call-by-value calculi and linear calculi that are both sound and complete.
[1995] attempted to add the ([Eta].v) rule to the call-by-value calculus, and the ([Eta].-o) and ([Eta].!) rules to the linear lambda calculus, they noted that the translation from the call-by-value calculus to the linear calculus does not preserve ([Eta].v).
