In Philip Wadler's "Monads and composable continuations" (published in Lisp and Symbolic Computation, 1994, doi.org/10.1007/BF01019944) the following continuation monad is defined:
- $type \hspace{0.2cm} M a = (a \rightarrow O) \rightarrow O$
- $unit :: a \rightarrow M a$
- $(\star) :: M a \rightarrow (a \rightarrow M b) \rightarrow M b$
- $eval :: M O \rightarrow O$
- $unit \hspace{0.2cm} v = \lambda c. c v$
- $m \star k = \lambda c.m (\lambda v. k v c)$
- $eval \hspace{0.2cm} m = m \hspace{0.2cm} id \hspace{0.5cm}[\text{where} \hspace{0.2cm} id = (\lambda v. v)]$
He then makes several claims in the passage below:
Here $O$ is the type of answers...
We have added one extra operation, $eval$, to the monad, which can be used to extract the answer from a ‘top-level’ computation. Substituting these definitions of $unit$ and $\star$ into the call-by-value monad translation and simplifying yields the usual call-by-value continuation-passing style translation. A pleasant property of this translation is that a source program is always given the same call-by-value semantics, regardless of whether the target program is given a call-by-value or call-by-name semantics.
Monads are in a sense just an abstraction of continuation passing style, and the second argument to $\star$ is very similar to a continuation. In a sense, we have continuations at two levels: at the meta-level, we have the continuation $k :: a \rightarrow M b$ and at the object level we have the continuation $c :: a \rightarrow O$.
Here are my questions:
What does he mean by the type of 'answers' and in what sense $eval$ extracts answers?
What does he mean by the "usual call-by-value continuation-passing style translation" and so what 'pleasant property' is he attributing to this translation?
What does he mean when he says that "Monads are in a sense just an abstraction of continuation passing style, and the second argument to $\star$ is very similar to a continuation"?
I think $O$ stands for 'Output', the set for possible outputs (or answers) of a 'program'.
We can regard functions of the form $X\to O$ as 'programs'.
Now, being of type $MA$ means that it is a program that inputs a program that inputs an object of type $A$. Let's call these 'computations' program analyser programs for now.
The unit of this monad $M$ assigns the 'evalutaion at $a$' function $\lambda f.fa$ to an object $a::A$. So that it is indeed of the form $A\to MA$.
The $eval$ function explicitly evaluates the identity function $id::O\to O$ at its input $m::MO$. Elements of $MO$ are program analysers for programs of input type $O$, which can be seen as the 'top level' computations, because they are 'postprocessing' the output.
The continuation passing style translation is a translation of programs that basically gets rid of returns, and thus get closer to the machine code order. The direct programming style is to use embedded function calls with return values. Take an example:
In the continuation style, instead of returns there's always a next call of a function, which has to be given as (the last) parameter in each and every function, including the basic operations. Supposed we have such basic operations $\ $+(a,b,k) :=k(a+b)$\ $ and $\ \ast$(a,b,k) :=k(a*b)$\ $, the previous example translates to something like:
Here $x$ will hold the result of application of $g$ to $20$.
Simply because this continuation monad $M$ is a specific example of monads, the monads can be viewed as abstractions of this.
Point 6. in definition of $M$ illustrates the continuation behavior.