{-# 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