{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
module Main (main) where
import HSXML_ext
import HSXML (h1)
main = runHTMLIO . run_root $ content
content =
standard_page
HeadAttrs {
ha_title = "Undelimited continuations are not functions",
ha_longtitle = "Undelimited continuations are co-values rather \
\than functions",
ha_description = "Undelimited continuations are often mis-represented \
\as functions, e.g., in Scheme. We explain the distinction \
\and describe the proper \
\undelimited continuation monad, which differs from \
\the one in Haskell's monad transformer libraries.",
ha_DateRevision = (9,August,2012),
ha_DateCreation = (14,February,2011),
ha_keywords = ["CPS", "undelimited continuation", "co-value",
"lambda-mu", "duality of computation"],
ha_links = HLinks
{
links_prev = FileURL "zipper.html",
links_next = FileURL "against-callcc.html",
links_up = FileURL "index.html",
links_other = []
}
}
(tdiv
(ul
(li (item'ref introduction))
(li (item'ref delim'undelim))
(li (item'ref contM))
(li (item'ref recursion'iteration))
(li (item'ref fix'callcc)
br nbsp)
(li (aref (FileURL "against-callcc.html")
"An argument against" (code "call/cc")))
)
hr
(describe introduction)
(describe delim'undelim)
(describe contM)
(describe recursion'iteration)
(describe fix'callcc)
)
introduction = DescriptionUnit "introduction"
(title "Undelimited continuations are not functions") $ tdu
(dbody
(tp[mup_text|
When one part of a program is being evaluated, producing the result,
the rest of the program lies ready to consume it. For example, in the program
|print 1 + 2*3|, the context |print []| is the consumer of the
result of the addition, and |print 1 + []| is the consumer for
the result of the multiplication. Whereas value is the meaning
of an expression, (undelimited) continuation is the meaning of a context.
Ever-present and implicit, continuations become explicit
when the program is converted to the
continuation-passing style (CPS) or when they are captured by a control
operator such as |call/cc|. Explicit continuations are often
represented as functions, which can be applied. One must keep
in mind however that an undelimited continuation is _not_ a genuine
function. It _does not return_, and hence cannot be meaningfully composed.|])
(p[mup_text|
We alert to the misconception of explicit, or first-class,
undelimited continuations as ordinary functions. The confusion is
wide-spread, for example, in the description and the code for the
|Cont| monad in Haskell's monad transformer libraries.
We argue for a better |call/cc| interface, to hopefully reduce
the bewilderment commonly associated with that control operator. We
describe the proper undelimited continuation monad, pointing out that
Haskell's |Cont| is actually the monad for _delimited_
continuations. Delimited and undelimited continuations are vastly
different. Delimited continuations are isomorphic to functions, they
do return the result and can be composed. We emphasize the great
help of types in understanding continuations and avoiding their surprises.|])
(p[mup_text|
Scheme's |call/cc| might be responsible for mistaking first-class
undelimited continuations as functions: the captured undelimited
continuation |k| in |(call/cc (lambda (k) ...))| indeed looks like
a function and can be applied to a value. It is not a genuine function
however. The expression |(k (k 1))|, albeit well-formed, is meaningless.
It makes as much sense to compose captured undelimited continuations
as to compose |abort| or |exit| `functions.' The |call/cc| interface
in SML is quite more helpful:|])
([mup_code|
type 'a cont
val callcc: ('a cont -> 'a) -> 'a
val throw: 'a cont -> 'a -> 'b|])
(tp[mup_text|
A captured continuation is represented as the value of an abstract type
|'a cont|. Since it is not a function, we need an operator, |throw|, to
pass the continuation a value to consume and so let it `continue.' The
type of |throw| is similar to the type of the exception-raising |raise|,
indicating that neither `function' returns.|])
(p[mup_text|
The untyped CPS transform might also make undelimited continuations
appear as functions. After all, they are represented as
functions -- in the metalanguage. One must clearly distinguish the
metalanguage, _in_ which the CPS code is written, from the object
language, _of_ which the CPS transform is taken.
Types make the distinction clear. An object-language expression
of the type |Int| has the CPS transform of the metalanguage
type |(Int->w)->w|, where |w| is the `answer-type'. An object-language
function, say, |Int->Bool|, is represented in CPS as the metalanguage
value of the type |(Bool->w) -> (Int->w)|. An object-level continuation
receiving the value |Int| has the metalanguage type |Int->w|.
The object-language continuation is represented as the metalanguage
function, whose type sets it apart from representations of
object-language functions.|])
(p[mup_text|
Distinguishing undelimited continuations and functions not only reduces
confusion but also gives a deep insight into the duality of
computation. A continuation is a co-value. Whereas a term, a producer,
has the type |t|, the context of the term -- the consumer, or the co-term --
can be given the type |NOT t|, isomorphic to |t -> Falsum|.
The answer-type |Falsum| has no constructors: Informally, it describes
the result of a crashed computer. The type of the
undelimited continuation |t -> Falsum|
clarifies that although the continuation may look like a function,
it never returns because there is no way to create a |Falsum| value.
In other words, the `result' of an undelimited continuation may never be
used by the program itself; it is `beyond the grave'.
Therefore, the value of the type |t -> Falsum| witnesses the
impossibility to produce a value of the type |t|. The type
|t -> Falsum| represents the proposition that is the negation
of that of |t|.|])
)
(references
(tp
"Pierre-Louis Curien and Hugo Herbelin: The duality of computation."
"ICFP 2000" br
(urlref (URL
"http://pauillac.inria.fr/~herbelin/publis/icfp-CuHer00-duality+errata.pdf"))
)
)
delim'undelim = DescriptionUnit "delim-vs-undelim"
(title "Vast difference between delimited and undelimited continuations")$ tdu
(dbody
(tp[mup_text|
Whereas an undelimited continuation is the meaning of the whole
context, a delimited continuation is the meaning of context's prefix,
mapping a context to a wider one. Despite sounding pretty much alike,
undelimited and delimited continuations are _qualitatively_
different. Since a delimited continuation is a mapping between
contexts, it may truly be a function, which returns and can be
composed. Undelimited continuations are not true
functions. Undelimited and delimited continuations also differ in
expressiveness, and this difference has been proven. First-class
_delimited_ continuations can express _any_ expressible computational
effect, including exceptions and mutable state. To be precise, any
effect that can be emulated by transforming the whole program (into
the state-passing--style, into an |Either|-returning style, etc.) can be
expressed with first-class delimited continuations without
the global transformation, see Filinski's ``Representing
Monads.'' In contrast, first-class undelimited continuations _cannot_
express raising and catching of exceptions. Furthermore, first-class
undelimited continuations, even when aided by exceptions, _cannot_
express mutable state. The limited expressiveness of undelimited
continuations has been proven by Hayo Thielecke, see the reference and
the abstract below.|])
(p[mup_text|
One sometimes hears a misleading statement that ``it is
possible to implement Scheme's |set!| in terms of Scheme's |call/cc|
and |letrec|.'' The statement mis-represents
Alan Bawden's observation that according to Scheme standards and common
practice, |letrec| is implemented in terms of |set!|; that hidden |set!|
can be `pried open' with |call/cc|. Of course |letrec| can be
implemented without |set!|, for example, via the fix-point combinator.
The inability of |call/cc| to express mutable state becomes clear
then. Section 4.4 of Friedman and Sabry's
``Recursion is a Computational Effect'' has the detailed explanation.|])
(p[mup_text|
One may wonder what is the use of first-class undelimited
continuations then. That is a good question. Many applications that
use |call/cc| also contain mutable cells holding continuations,
betraying the well-known Filinski's emulation of delimited control via
|call/cc| and a mutable cell. Undelimited continuations by themselves
are hardly practically useful. The best non-trivial application of
bare |call/cc| is along the lines of Nick Benton's ``Undoing Dynamic
Typing.'' The paper mentions at the end that in practice `undoing'
should be done within transaction boundaries. The latter calls for
delimited continuations. Given that first-class delimited
continuations -- often emulated via |call/cc| together with |set!| --
are strictly more expressive than undelimited ones, and most often used
in practice, one would think that |call/cc| should have been replaced
by a delimited control operator.|])
)
(references
(tp
"Andrzej Filinski: Representing Monads. POPL 1994." br
(urlref (URL
"http://www.diku.dk/~andrzej/papers/RM-abstract.html")))
(p
"Hayo Thielecke: Contrasting Exceptions and Continuations. 2001" br
(urlref (URL "http://www.cs.bham.ac.uk/~hxt/research/exncontjournal.pdf"))
br
[mup_text|
Abstract: ``Exceptions and first-class continuations are the most
powerful forms of control in programming languages. While both are a
form of non-local jumping, there is a fundamental difference between
them. We formalize this difference by proving a contextual equivalence
that holds in the presence of exceptions, but not continuations; and
conversely, we prove an equivalence that holds in the presence of
continuations, but not exceptions. By the same technique, we show that
exceptions and continuations together do not give rise to state, and
that exceptions and state do not give rise to continuations.''|])
(p
"Daniel P. Friedman and Amr Sabry: Recursion is a Computational Effect."
br
"Tech. Rep. TR546, Computer Science Department, Indiana University,"
"December 2000." br
(urlref (URL
"http://www.cs.indiana.edu/~sabry/papers/recursion-monads-tr.pdf"))
)
(p
"Nick Benton: Undoing Dynamic Typing. FLOPS 2008." br
(urlref (URL "http://research.microsoft.com/~nick/newtrans.pdf"))
)
)
{-
refer to Hayo's work: answer-type polymorphism and purity.
> The reason is indeed because of "effect polymorphic", i.e.
> there has to be an underlying parametricity theorem which tells you that
> the only truly effect polymorphic functions are the pure ones, for
> basically the same reason that the only function of type forall a.a->a
> is the identity. Do you know if such parametricity theorems have been
> proved?
I think it might be this work
@InProceedings{ thielecke-control,
author = "Hayo Thielecke",
title = "From Control Effects to Typed Continuation Passing",
pages = "139--149",
crossref = "popl2003",
url = "http://www.cs.bham.ac.uk/~hxt/research/effects.pdf",
abstract = "First-class continuations are a powerful computational
effect, allowing the programmer to express any form of jumping.
Types and effect systems can be used to reason about continuations,
both in the source language and in the target language of the
continuation-passing transform. In this paper, we establish the
connection between an effect system for first-class continuations and
typed versions of continuation-passing style. A region in the
effect system determines a local answer type for continuations,
such that the continuation transforms of pure expressions
are parametrically polymorphic in their answer types.
We use this polymorphism to derive transforms that make use of effect
information, in particular, a mixed linear\non-linear continuation-passing
transform, in which expressions without control effects are passed
their continuations linearly."
}
I have just noticed a recent paper
author = "Hayo Thielecke",
title = "Control Effects as a Modality",
journal = j_jfp,
year = 2009,
volume = 19,
number = 1,
pages = "17--26",
which I haven't even skimmed.
-}
contM = DescriptionUnit "proper-contM"
(title "Monads for undelimited continuations") $ tdu
(dbody
(tp[mup_text|
The proper implementation of _undelimited_ continuations is
surprisingly tricky. In particular, the |Cont| monad in Haskell's
monad transformer library has a couple of imperfections.
Our ideal monad for undelimited continuations: (i) spells out
in syntax and types of its operations that undelimited continuations
are not be treated as functions; (ii) statically prevents
building or executing computations that break undelimited continuation
abstraction and depend on the answer-type. We eventually develop
two implementations satisfying both requirements; the second one
is almost the same as |Cont|.|])
(p[mup_text|
The |Cont| monad in the popular Haskell monad transformer library
does not satisfy the requirements. The captured continuation has the
type of a monadic function. The |Cont| documentation (through the
current version 2.0.1.0) confirms that view, saying ``Computations are
built up from sequences of nested continuations, terminated by a
final continuation (often id) which produces the final result.
Since continuations are functions which represent the future of
a computation...'' We have already argued that
undelimited continuations are not functions and that one should
forget about the ``final result.'' It behoves for a typed language
to statically enforce the forgetting. Incidentally, in the presence
of first-class undelimited continuations, computations can no longer be
viewed as ``sequences of nested continuations.'' As Peter Landin
said, ``You can enter a room once, and yet leave it twice.''
Our code will show a simple example.|])
(p[mup_text|
Recall that monad is a technique of embedding an impure, object language,
into a pure functional (meta)language. For an object language
with control effects, the well-known embedding technique is
continuation-passing style (CPS) --
which is what all our monads implement. In CPS, an object
language expression of the base object type |a| is represented
as a Haskell value of the type |(a -> w) -> w| where |w|
is a so-called `answer-type', to be discussed shortly.
An object-language |a->b| function is represented as Haskell's
|a -> ((b->w) -> w)| function. An object-language co-value of
the type |a|, that is, the continuation consuming |a| value
is represented in Haskell
as the value of the type |a->w|. We stress
that although the representation of an object language
continuation is a Haskell function, it differs, in type, from
the representation of any object language function. CPS operations
for building primitive computations, extending them, capturing an
undelimited continuation and invoking it have the following form:|])
([mup_code|
return x = \k -> k x
m >>= f = \k -> m (\v -> f v k)
callCC f = \k -> f k k
throw k x = \_ -> k x|])
(p[mup_text|
All our monads share the above code, modulo |newtype|-induced
conversions. The monads differ in their treatment of the answer-type |w|.
An object-language computation cannot know what |w| is; to it, |w|
is arbitrary. This fact gives us the first implementation, with the following
types for monadic values and continuations:|])
([mup_code|
newtype CPS1 a = CPS1{unCPS1:: forall w. (a -> w) -> w}
type K1 a = forall w. a -> w|])
(tp[mup_text|
Alas, we cannot write |callCC|:|])
([mup_code|
callCC1 :: (K1 a -> CPS1 a) -> CPS1 a
callCC1 f = CPS1 $ \k -> unCPS1 (f k) k|])
(tp[mup_text|
The type-checker keeps complaining that
the code for |callCC| identifies |w| quantified in the type of |CPS1|
with |w| quantified in the type of |K1|. The type-checker has the point.
The answer-type is the type of the value of the crashed computer; the program
cannot make any use of that value, or care of that type. Ostensibly that
is what the types |CPS1| and |K1| say, that the answer-type
is arbitrary. It cannot be totally arbitrary however: the continuation
captured by |callCC| leads to the same crashed computer value as the
computation whose continuation has been captured. The code for |callCC1|
says that the answer-type
of the captured |K1| must be the same as that of |CPS1|. The signature of
|callCC1| has no way to express that constraint.|])
(p[mup_text|
A different way to introduce a type whose values cannot be used
is to define an algebraic data type with no constructors -- an empty
type (disregarding bottom). Monadic values and continuations get the
following types:|])
([mup_code|
data Falsum -- no constructors
newtype CPS2 a = CPS2{unCPS2:: (a -> Falsum) -> Falsum}
type K2 a = a -> Falsum|])
(tp[mup_text|
with indeed the same answer-type, |Falsum|.
Even the program knows that, but it cannot get its values since none exist.
The type-checker now accepts the definitions of all four operations; we can
write any computation with undelimited control effects. Alas, we cannot
execute these computations. To execute a |CPS2 a| computation,
we need the initial continuation |a -> Falsum|.
We cannot construct values of that type: |Falsum| really has no constructors.
The initial continuation (whose invocation leads to the crashed computer,
eventually) should be supplied by the operating or the run-time system.
GHC RTS does supply it.|])
(p[mup_text|
Cheating is always an option. We can run the computation and obtain
its result through a side-channel. Since the side-channel is an effect,
we need another monad:|])
([mup_code|
newtype CPS3 m a = CPS3{unCPS3:: (a -> m Falsum) -> m Falsum}
type K3 m a = a -> m Falsum|])
(tp[mup_text|
The following code of the |run| operation instantiates |m|
to |ST s|, using a mutable cell to stash away the result of the computation.
The code exhibits lots of partiality, which is inherent, betraying the
essential cheating. Instead of |ST s|, we could have used the Error
monad |Either a|.|])
([mup_code|
runCPS3 :: (forall m. CPS3 m a) -> a
runCPS3 m = runST (do
res <- newSTRef (error "Continuation has escaped!")
unCPS3 m (\v -> writeSTRef res v >> return undefined)
readSTRef res)|])
(tp[mup_text|
We stress the higher-rank type of |runCPS3|: we introduced the monad
|m| only for the sake of |runCPS3|. The rest of the monadic computation
should stay away from it. The quantification over |m| keeps the program
away from using |m| in any way whatsoever.|])
(p[mup_text|
The implementation |CPS3| looks suspiciously like |Cont| in the
monad transformer library MTL, with the side-channel monad |m| playing
the role of the answer-type |w|. Neither should be looked at
by computations. We obtain the final implementation|])
([mup_code|
newtype Cont w a = Cont{unCont:: (a -> w) -> w}
type K w a = a -> w
callCC :: (K w a -> Cont w a) -> Cont w a
callCC f = Cont $ \k -> unCont (f k) k
throw :: K w a -> a -> Cont w b
throw k x = Cont $ \ k_ignored -> k x
runCont :: (forall w. Cont w a) -> a
runCont m = unCont m id|])
(p[mup_text|
The first difference from the monad-transformer library is the type
of the captured continuation, |K w a|, corresponding to no object
function. Therefore, we need a special operation to invoke the
continuation: |throw|. Our implementation thus emphasizes in syntax
and in types the difference between undelimited continuations and
functions. The second, main difference is the higher-rank type of
|runCont|, ensuring that computations really not have looked at the
answer-type. The answer-type is fixed all throughout, yet a
computation cannot know what it is. Therefore, we may chose |w| as we
wish -- and we do, after the program has been constructed. The
higher-rank type of |runCont| also prevents the program from using
|runCont| internally to run parts of its computation. No such
restriction exists for MTL's |runCont|, telling us that the latter is
the monad for _delimited_ continuations.|])
)
(version "February 2011")
(references
(tp
(file'ref "CPSs.hs")
"Complete Haskell code for the four implementations of the"
"monad of undelimited continuations. The code includes several"
"examples."))
recursion'iteration = DescriptionUnit "iter-recur"
(title "Recursion from Iteration") $ tdu
(dbody
(tp[mup_text|
Recursion from iteration, first presented by Andrzej Filinski at
the Continuation Workshop 1992, is a neat rare example of
undelimited continuations alone sufficing. The journal paper developed the
example further, making it an excellent illustration for the duality
of computation. The original example was in ML. We recast it
in terms of monads, in Haskell, demonstrating equational forward
and backward reasoning. The example also
shows off the Haskell library of proper undelimited
continuations developed above.|])
(p[mup_text|
Following Filinski, we define _iteration_ as a tail-recursive function
|loop|; general recursion is represented by the fix-point combinator:|])
([mup_code|
loop1 :: (a -> a) -> (a -> b)
loop1 g = \x -> loop1 g (g x)
fix1 :: ((a->b) -> (a->b)) -> (a->b)
fix1 f = \a -> f (fix1 f) a|])
(tp[mup_text|
By unrolling the definitions, we see that|])
([mup_code|
loop1 g = g . g . g . g ...
fix1 f = f $ f $ f $ f ...|])
(tp[mup_text|
giving us the first hint of their duality. Iteration, |loop|, as
a particular case of recursion, can be expressed via fix|])
([mup_code|
loop1' g = fix1 (. g)|])
(tp[mup_text|
verified by simple equational reasoning. The main
question is expressing |fix| via |loop|.|])
(p[mup_text|
A moment of reflection tells us that writing |fix| in terms of |loop|
must be possible. After all, any recursive program, however general,
is going to be executed on a CPU, which runs in a simple tail-recursive
loop. Such a low-level view gives us the second hint: we need to explicitly
deal with the stack pointer, saving and restoring return addresses.
The stack pointer pointing to
the stack with the saved return address is one realization of undelimited
continuations. We indeed have to have some control effect to escape
from the infinite |loop|: most useful general recursion programs terminate.
Since we will be dealing with effects, we have to introduce monads,
re-writing our definitions of |loop| and |fix|:|])
([mup_code|
loop :: Monad m => (a -> m a) -> (a -> m b)
loop g = \x -> g x >>= loop g
fix :: Monad m => ((a -> m b) -> (a -> m b)) -> (a -> m b)
fix f = \x -> f (fix f) x|])
(tp[mup_text|
The definition of |fix| remains the same, with only the type specialized.
According to its type our |fix| is the _applicative_ fix-point combinator
(like the one typically used in strict languages), to be distinguished
from the very different, lazy |mfix| of Haskell. Here is an example
of using fix:|])
([mup_code|
fact2 :: Monad m => (Int -> m Int) -> (Int -> m Int)
fact2 self n = if n == 0 then return 1 else liftM (n *) (self (n-1))
fact2r = fix fact2 5 >>= print|])
(tp[mup_text|
defining the factorial with open recursion in an arbitrary monad.
We tie the knot and run it in the |IO| monad, printing the result.|])
(p[mup_text|
As before, iteration is easily expressed in terms of the more general
recursion:|])
([mup_code|
loop' g = fix (\s x -> g x >>= s)|])
(tp[mup_text|
The proof is easy, by equational reasoning:|])
([mup_code|
loop' g
= fix (\s x -> g x >>= s) {- definition of loop' -}
= (\s x -> g x >>= s) (fix (\s x -> g x >>= s)) {- definition of fix -}
= (\s x -> g x >>= s) (loop' g) {- definition of loop' -}
= \x -> g x >>= (loop' g) {- beta-reduction -}
= loop g {- definition of loop -}
|])
(p[mup_text|
We now search for an expression of fix in terms of loop.
We will be using a monad of undelimited continuations:|])
([mup_code|
newtype CPS3 m a = CPS3{unCPS3:: (a -> m Falsum) -> m Falsum}|])
(tp[mup_text|
For clarity, we will drop |CPS3| and |unCPS3| conversions,
which operationally the identity anyway. The monad operations take the
following form then:|])
([mup_code|
return x = \k -> k x
m >>= f = \k -> m (\v -> f v k)
callCC f = \k -> f k k
throw k x = \_ -> k x|])
(tp[mup_text|
We solve the problem by equationally deriving a constructive proof
of the proposition|])
([mup_code|
forall f x k. exists h y. fix f x k = loop h y k|])
(tp[mup_text|
stating that |fix| is expressible via |loop| in the continuation monad.
Skolemizing, we obtain|])
([mup_code|
fix f x k = loop (h f x k) (y f x k) k|])
(tp[mup_text|
We need to find such functions |h| and |y| that the equality above
holds for the arbitrary |f|, |x|, and |k|.|])
(p[mup_text|
Unrolling |fix| and |loop| and inlining the definition of |(>>=)| from
the above, gives further equalities|])
([mup_code|
f (fix f) x k = (h f x k) (y f x k) (\v -> loop (h f x k) v k)
f (\x1 k1 -> loop (h f x1 k1) (y f x1 k1) k1) x k
= (h f x k) (y f x k) (\v -> loop (h f x k) v k)|])
(tp[mup_text|
We have to match |(\x1 k1 -> loop ...)| on the left-hand-side
with |(\v -> loop (h f x k) v k)| on the right-hand-side.
The first function receives two independent pieces of data,
so the second should too. Thus |v| must be a pair, |(x,k)|;
the invoking function |h| will uncurry. The hint
that loop's argument, the `state' to be repeatedly
transformed by the loop function, must be a pair |(x,k)|
comes also from the low-level point of view.
Recall that |x| is the argument of the recursive
function, and |k| is its continuation, the stack with the
return address on it. Together, |(x,k)| is the stack frame:
the argument plus the return address. A processor running in a loop
is indeed a frame transformer.|])
(p[mup_text|
Letting |v| be a pair gives us|])
([mup_code|
f (\x1 k1 -> loop (h f x1 k1) (y f x1 k1) k1) x k
= (h f x k) (y f x k) (\(x1,k1) -> loop (h f x k) (x1,k1) k)|])
(tp[mup_text|
To match the two loop expressions in parentheses, we have to define|])
([mup_code|
y f x k = (x,k)
h f x k = h' f|])
(tp[mup_text|
that is, |h| should not depend of |x| and |k| arguments; |h'| is
to be determined. Substituting these definitions, we obtain|])
([mup_code|
f (\x1 k1 -> loop (h' f) (x1,k1) k1) x k
= (h' f) (x,k) (\ (x1,k1) -> loop (h' f) (x1,k1) k)|])
(tp[mup_text|
We need an auxiliary lemma:|])
([mup_code|
loop g x k = loop g x k1|])
(tp[mup_text|
for any |g|, |x|, |k|, |k1|. In other words, |loop| never invokes
its continuation and therefore can be given any: |loop| loops and
never returns. We can easily prove the lemma by co-induction.
Applying the lemma gives|])
([mup_code|
f (\x1 k1 -> loop (h' f) (x1,k1) k1) x k
= (h' f) (x,k) (\ (x1,k1) -> loop (h' f) (x1,k1) k1)|])
(tp[mup_text|
which can be read (after flipping) as the definition for the
sought |h'|:|])
([mup_code|
h' f (x,k) k2 = f (\x1 k1 -> k2 (x1,k1)) x k|])
(p[mup_text|
We are done. We would like to polish the result: during the derivation,
we broke the monadic abstraction, replacing bind and return
of the CPS monad with their concrete expressions. We want to get
the abstraction back, re-introducing |(>>=)| and |return|.
They won't be enough, as we can see by comparing the pattern
of using |k| in these operations with the pattern in |h'|.
Our |h'| not just passes the received continuation around or immediately
invokes it. It also stores continuations in
data structures (pairs). Our resulting expression:|])
([mup_code|
fix f x k = loop (h' f) (x,k) k|])
(tp[mup_text|
can be re-written, using the definition of |callCC| from above, as|])
([mup_code|
fix :: ((a -> CPS3 m b) -> (a -> CPS3 m b)) -> (a -> CPS3 m b)
fix f x = callCC (\k -> loop (h' f) (x,k))|])
(tp[mup_text|
The definition of |h'| can be likewise transformed in these steps:|])
([mup_code|
h' f (x,k) k2 = f (\x1 k1 -> k2 (x1,k1)) x k
h' f (x,k) k2 = f (\x1 -> callCC (\k1 -> throw k2 (x1,k1))) x (\v -> k v)|])
(tp[mup_text|
giving us the final result:|])
([mup_code|
h' :: ((a -> CPS3 m w) -> (b -> CPS3 m w))
-> ((b, K3 m w) -> CPS3 m (a, K3 m w))
h' f (x,k) = callCC (\k2 ->
f (\x1 -> callCC (\k1 -> throw k2 (x1,k1))) x >>= (\v -> throw k v))|])
(tp[mup_text|
The result is achieved by equational reasoning and is correct by construction.
It has indeed worked the first time.|])
(p[mup_text|
The type of |h'| makes _classical_ logical sense, expressing the proposition|])
([mup_code|
(f1 -> f2) = (NOT f1 -> NOTNOTNOT f2)|])
(tp[mup_text|
keeping in mind that |K3 m w| is logically |NOT w|, reading |CPS3 m|
as double-negation, and using|])
([mup_code|
K3 m (b -> CPS3 m w)
~ NOT (b -> NOTNOT w)
= NOT (NOT b OR (NOTNOT w)) = b AND (NOT w)
~ (b,K m w)|])
(p[mup_text|
What is left to prove is the fix-point thus obtained being the least one,
or the related property of universality. See Filinski's paper for details.|])
-- The monadic approach does help: the premise of the proof is that the
-- function |f| whose fix-point we seek, is rigid??
-- This property is equivalent?? to saying that although |f| has the
-- monadic type, it is pure. One can see why it matters: if |f| is allowed
-- mutations, it can easily distinguish a fix-point combinator that relies
-- on unrolling (such as ours) from the fix-point combinator relying on sharing
-- (which is typical of combinators implemented via built-in value recursion).
-- However, if we require |f| to be polymorphic over the monad, then
-- |f| is effectively pure. It cannot use any monadic operations but
-- |return| and |bind|.
-- We need delimited continuations so to obtain that even a pure
-- function using fix is pure. So, to use parametricity for
-- the proof we need delimited control!
(p[mup_text|
The original version of this article was written in early 2003, in
Scheme, after the independent re-discovery of recursion via iteration.
Unlike Filinski's, our derivation was directly in terms of |call/cc|
rather than the |C| operator.
The main hint probably came from the CPU point of view. The original
version too relied on equational reasoning. The present version
uses Haskell, which permits equational reasoning on the code itself.
We no longer have to translate Math into code; Math is code. The monadic style
also gives a shorter derivation.|])
)
(version "(original) February 2003; (monadic) February 2011")
(references
(tp
"Andrzej Filinski: Recursion from Iteration" br
"Lisp and Symbolic Computation, vol. 7, no.1, pp. 11-38 (January 1994)" br
(urlref (URL
"http://www.diku.dk/hjemmesider/ansatte/andrzej/papers/RfI.ps.gz"))
)
(p
(file'ref "IterRec.hs")
"Complete Haskell code for all the fragments mentioned in the article."
"The code contains several more examples, of nested and higher-order"
"fix-points, mentioned in Filinski's paper.")
(p
(item'ref fix'callcc) br
"In Scheme, we can obtain general recursion from" (code "call/cc")
"alone, without any loop. Types are again revealing, that"
"the application of" (code "call/cc") "to the identity has the recursive"
"type.")
(p
(aref (FileURL "../Computation/fixed-point-combinators.html")
"Many faces of the fixed-point combinator") br
"The web page points to several ways of defining the fix-point combinator"
"in OCaml and Haskell without value recursion or iteration.")
)
-- type: double-neg elimination (p31)
-- Looping in the direct-style corresponds to the fix-point in CPS.
-- (p32 and earlier)
fix'callcc = DescriptionUnit "fix-callcc"
(title "Self-application as the fixpoint of" (code "call/cc")) $ tdu
(dbody
(tp[mup_text|
Truly |call/cc| and the fix-point combinator |Y| are two sides of the
same coin. The following article makes the claims formal and proves
them. Two examples in the article demonstrate that first-class
continuations can be really tricky, and so being formal helps. For
proofs we rely on syntax-rules macros: one macro does a
continuation-passing-style (CPS) transform, and another simple macro
-- which is actually a lambda-calculator -- normalizes the result of
the transform.|])
(p "Theorem: The following expressions are observationally"
"equivalent in call-by-value untyped lambda-calculus.")
(ul
(li (code "((call/cc ... (call/cc call/cc)) p)"))
(li (code "((call/cc ... (call/cc (call/cc id))) p)"))
(li (code "((lambda (x) (x x)) p)")))
(tp[mup_text|
Here |p| is a value; |(call/cc ...)| signify zero or more
applications of |call/cc|, and |id| is the identity function. The
article also discusses self-applications of delimited continuation
operators.|])
(p[mup_text|
In this article, continuations, fixpoints, CPS, higher-order syntax,
syntax-rule macros and lambda-calculators all come together.|])
)
(references
(tp
(aref (FileURL "../Scheme/callcc-calc-page.html")
"Normal-order direct-style beta-evaluator with syntax-rules,"
"and the repeated applications of call/cc"))
(p
(file'ref "../Scheme/callcc-fixpoint.txt")
"Self-application as the fixpoint of call/cc" br
"The first version of the article, posted on the newsgroup"
(code "comp.lang.scheme")
"on Thu, 18 Sep 2003 23:39:02 -0700")
)
-- LocalWords: Undelimited undelimited SML callcc Bool Falsum Filinski's
-- LocalWords: Monads proven letrec Filinski parametricity Landin callCC
-- LocalWords: monads newtype forall unCPS runCont Andrzej equational