Odtnhj

the Cont r a type stands for a function which takes a continuation a->r and produces a result of type r. So both the continuation and the entire Cont r a produce a result of the same type r.

My question is: are the two results necessarily the same value, or can a Cont r a post-process the result from the continuation and produce a different value, albeit of the same type r?

I tried using (+1) for post-processing (note the + 1 --<--):

c1 :: Int -> Cont r Int
c1 x = let y = 2*x
 in cont $ k -> (k y) + 1 --<--

Now that doesn't typecheck, because my post-processing function (+1) only accepts an argument whose type belongs to the Num typeclass. However, I pass the result of the continuation (k y) which is of some type r that is not guaranteed to belong to the Num typeclass.

Whatever I do to (k y), it must be a function of type r->r. The only function which can do this for all r is the id function and using id for post-processing is no post-processing at all.

However, the whole thing does typecheck if I restrict r to the Num typeclass or even to the concrete type Int. It then produces the expected result:

*Main> runCont (c1 1) id
3

I am quite unsure,

• if such post-processing and restricting the type of r is a normal thing to do, and if so, in what circumstances this might be useful


• or if the type variable rhas to be read as for all r and restricting the type of r will lead to all sorts of trouble.

Can someone shed some light on this?

Technically, I think it's fine. Specializing Cont r a to Num r => Cont r a doesn't seem fundamentally more problematic than specializing Reader r a to Num r => Reader r a.

An implication of doing so is that the resulting CPS computation can only be run against a (final) continuation that produces a number, but that's obvious -- if you have a computation that post-processes the continuation result as a number, it can only be used with continuations that produce numbers!

As additional evidence that this is sanctioned at least to some degree, note that there's a function:

mapCont :: (r -> r) -> Cont r a -> Cont r a

If this function was to be used with no restriction on r, the only valid values for its first argument would be id or functions that don't terminate, as you have noted.

A version of your c1 using mapCont might look like:

c2 :: (Num r) => Int -> Cont r Int
c2 x = mapCont (+1) $ return (2*x)

and seems to work fine:

> runCont (c2 10) id
21
> runCont (c2 10) (const 5)
6
> runCont (c2 10) show
... No instance for (Num String) arising from a use of 'c2' ...

As for when this would be useful, I'm not sure. I can think of a few somewhat lame applications. You could define an computation that overrides the final result (provided no other kind of post-processing is used):

override x = cont (const x)

to be used like:

> runCont (return 2 >>= x -> cont (f -> f (x*3))) id
6
> runCont (return 2 >> override 1000 >>= x -> cont (f -> f (x*3))) id
1000
>

or a computation transformer that emulates a writer to add log functionality:

annotate note comp = mapCont ((a, w) -> (a, note:w)) comp

which you might use like this:

runCont (annotate "two" (return 2)
 >>= x -> annotate "times three" (cont (f -> f (x*3))))
 (a -> (a, ))

yielding:

(6,["two","times three"])

These don't seem like very compelling applications, though.

@KABuhr has shown that post-processing in the ordinary Cont works, but didn't find "very compelling applications". I'm going to show you how post-processing is useful, but it only works best when you generalize Cont. First, some header stuff (mostly used in the examples):

-# LANGUAGE RebindableSyntax #-

import Prelude(Num(..), Eq(..), Enum(..))
import Data.Bool
import Data.Function
import Data.Functor.Identity
import Data.List
import Data.Maybe
import Data.Tuple

import Control.Lens(_1, _2, traversed)

Now, a generalized Cont.

newtype Cont r f a = Cont runCont :: (a -> r) -> f 

Your question was "is post-processing allowed in Cont?" The answer is yes. If would like it to not be so, you can use newtype ContS a = runContS :: forall r. (a -> r) -> r which totally disallows it. In fact, ContS a is isomorphic to a. The Cont I just defined takes the opposite position: even type-changing post-processors are allowed. We can define a standard Functorial (<$>).

infixl 1 <$>
(<$>) :: (a -> b) -> Cont r f a -> Cont r f b
f <$> Cont x = Cont $ cont -> x $ realX -> cont (f realX)

Before continuing, let's get an understanding of the metaphor behind Cont. A Cont r f a is a computation that can produce as. It will give you the as, but will ask you to produce rs. Once you do that, it'll make fs. It's sort of like a (r -> f, a), but with heavy restrictions on use. If we try to define an Applicative-ish operator, we see something interesting.

infixl 1 <*> 
(<*>) :: Cont m f (a -> b) -> Cont r m a -> Cont r f b
Cont f <*> Cont x = Cont $ cont -> x $ realX -> f $ realF -> cont (realF realX)

(<*>) is sort of doing two operations at once. It is applying the a -> b to an a to get b, but it's also composing the m -> f and r -> m aspects into a r -> f part. However, the type of (<*>) no longer fits into the normal Applicative format. This is why we use Cont r a instead of Cont r f a. The former is less powerful, but it fits into our existing framework. To get our Cont to work, we have to leave some of the established infrastructure behind.

Before we get into the RebindableSyntax-level stuff, here's some usage.

complete :: Cont a f a -> f
complete (Cont x) = x id

amb :: [a] -> Cont (Maybe b) (Maybe (a, b)) a
amb = Cont (const Nothing)
amb (x : xs) = Cont $ test -> case test x of
 Nothing -> runCont (amb xs) test
 Just y -> Just (x, y)
poly :: Num a => a -> a -> a -> a
poly x y z = sq x * y + sq y + z + sq z * x
 where sq x = x * x
solution :: (Num a, Enum a, Eq a) => Maybe (a, (a, (a, ())))
solution = complete $ testRoot <$> amb [-5..5]
 <*> amb [-10 .. -5]
 <*> amb [5..10]
 where testRoot x y z = case poly x y z of
 0 -> Just ()
 _ -> Nothing

complete completes a computation when there isn't actually a gap holding it up. amb takes a [a], and goes through each a, one by one. It passes each into the test, and searches until it finds one that succeeds. It post-processes the result of the test in two ways. It resets the result until it's a Just (or gives up), and a Just result gets up paired with the input that built it.

In solution, the complete is delimiting the extent of the continuation passed to the ambs. Each amb is passed the code that lies between it and the complete. E.g., the continuation given to the amb [-5..5] is x -> testRoot x <*> amb [-10 .. -5] <*> amb [10..5]. This style of continuations is called shift/reset. Cont is shift, complete is reset. The idea is that amb [-5..5] is a "liar"; it "looks like" a Num a => a because it's getting passed to testRoot, but it's actually a control structure that turns everything around it inside-out. Compared to the normal Cont r a, the control structures allowed in our Cont are more powerful.

Now, here's what we need RebindableSyntax for:

(=<<) :: (a -> Cont r m b) -> Cont m f a -> Cont r f b
f =<< Cont x = Cont $ cont -> x $ realX -> runCont (f realX) cont
(>>=) = flip (=<<)
return :: a -> Cont r r a
return x = Cont ($ x)

(=<<) is the Monad-style function application operator. Again, our version doesn't fit the usual type. With (>>=) and return, do-notation has now been redefined to work with Cont. You can go back and rewrite solution in do-notation to see that it works.

Let's really get out there. The idea behind profunctor optics is that data structures give rise to "transformer transformers". E.g. a Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t takes a transformer between the "small" structures a and b and makes one from between the "bigger" s and t. Look what lies just a flip away...

editing :: ((a -> Identity b) -> s -> Identity t) -> s -> Cont b t a
editing optic x = Cont (runIdentity . flip optic x . (Identity .))

editing, as a control structure, takes a reference to a field inside a structure, a structure to use it on, and then mutates that structure with "the rest of the program." Using it, you can write the following:

example :: (a -> a) -> [(Bool, (a, a))] -> [(Bool, (a, a))]
example f xs = complete $ do x <- editing traversed xs
 n2 <- editing _2 x
 n <- case fst x of
 True -> editing _1 n2
 False -> editing _2 n2
 return (f n)

I hope, with even these contrived examples, that you're convinced that post-processing is useful in Cont. There's nothing wrong with doing it. However, if you want to use it at its full potential, you have to break out of the existing Applicative and Monad form. This is painful, so we cripple Cont to make it fit, disabling type-changing post-processing as a trade-off.