The continuation-passing style means your program does not give its answer directly (“the direct style”, what you've always done); instead, your program takes one more parameter, a function parameter k, and your program's last job is to call k with the answer. We say that k is the continuation, and this is why we say this style continuation-passing—your user passes a continuaton to your program. (And your program may be using a subprogram, and so you may be passing some continuation to that, too.)
If you ask what's the difference from callbacks? Right, same difference!
What happened was that this same idea was cool among researchers, who coined “continuation”, before it was cool among programmers, who coined “callback”.
Here is a very boring example (but least distraction) of defining programs that answer 1, showing both the direct style and the continuation-passing style.
-- Direct style. one_ds :: Integer one_ds = 1 -- Continuation-passing style. one_cps :: (Integer -> r) -> r one_cps = \k -> k 1 -- Or, one k = k 1
How about an actual function such that the answer varies with the input? Here is a squaring function in the continuation-passing style (though not completely):
square_cps1 :: Integer -> (Integer -> r) -> r square_cps1 x = \k -> k (x * x)
Why I said not completely: See how I was using (*), a
direct-style multiplier? Now, I am not saying that you must never mix the two
styles; you mix them as you see fit. But I want to show you what things look
like when you use a subprogram that has a continuation-passing interface,
and one of the least-setup ways is to imagine that even some built-in arithmetic
you need is in the continuation-passing style, like this:
mul_cps :: Integer -> Integer -> (Integer -> r) -> r -- Specification: @mul_cps m n k@ calls k with the product of m and n. -- Imagine it's the built-in multiplier. -- But for the sake of experimenting, I make: mul_cps x y = \k -> k $! (x * y) -- The $! kills laziness and is probably a good idea for arithmetic.
So what I need to do for squaring: I receive from my user a number
x and a continuation k, and my job is to ensure that
somehow k is called with the square of x. Ah! I will
have mul_cps do both the multiplying and the calling for me.
square_cps2 :: Integer -> (Integer -> r) -> r square_cps2 x = \k -> mul_cps x x k
That was the first example of you calling a subprogram (mul_cps)
and passing a continuation to it. It was also a boring one in the sense that
you just pass your user's k verbatim to the subprogram. Below is an
example where you have to improvise a new continuation.
Write a function to square the input and add one. Assume that the built-in adder is in only the continuation-passing style (but fortunately 1 is still provided directly rather than the zealotry of one_cps):
add_cps :: Integer -> Integer -> (Integer -> r) -> r -- Specification: @add_cps m n k@ calls k with the sum of m and n. -- Imagine it's the built-in adder. -- But for the sake of experimenting, I make: add_cps x y = \k -> k $! (x + y)
You can pass the user's number x twice to mul_cps,
but what continuation should you pass? This continuation has to be written by
you, because you are the one saying you are not done yet, you still have to add
one. (And then you are done and you are ready to call your user's continuation.)
So, you write this continuation yourself to say: Take the received answer
s (you know it's x²), give it to add_cps
along with 1 for adding, and the sum is to be sent to your user's
k.
squareplus1_cps :: Integer -> (Integer -> r) -> r squareplus1_cps x = \k -> mul_cps x x (\s -> add_cps s 1 k)
Here is one last example in this section. Write a function to compute x²(x²+1). This illustrates non-linear dataflow (s = x² is required by two stages). I will just give my unexplained solution; you try to explain it, or even better, you try to solve it yourself first for exercise.
f_cps :: Integer -> (Integer -> r) -> r f_cps x = \k -> mul_cps x x (\s -> add_cps s 1 (\t -> mul_cps s t k))
It is a good question to ask: Why do we care about the continuation-passing style? Especially since it can be quite verbose and mind-bending.
There was a time when compilation and code optimization for functional languages were easier on continuation-passing code. Now, this did not mean they asked you to write in this style yourself; it meant that you would still write in the direct style, then the compiler would translate to the continuation-passing style mechanically and process it further. There were a lot of papers by Andrew Appel on this.
There was a time when heap size was artificially unlimited and stack size was artificially limited. (A reasonable limitation from the OS for sure, but could have been easily abstracted away in high-level languages—the whole point of “high-level”—except most implementers didn't care.) The workaround was the continuation-passing style because it uses the heap where the direct style uses the stack.
Example: In this direct-style code
f x = g x + x
since the g x is not a tail call, the call stores on the
stack the address of the ? + x code—the return address. In
general, a non-tail call causes an “activation record” on the stack
containing the return address, parameters (if not in registers), and local
variables (if not in registers).
The continuation-passing style version
f_cps x = \k -> g_cps x (\y -> add_cps y x k)
doesn't use as much stack space because all calls are tail calls. But how
is \y -> add_cps y x k represented as a parameter?
Firstly there is a code pointer for sure. Then note that x
and k are from the outside scope, so they need to be stored too.
The whole package is known as “closure”, and since we are avoiding the stack,
the closure is stored on the heap, and its address is passed to
g_cps.
In general, whereas non-tail calls in the direct style produce activation records on the stack, their translations to the continuation-passing style produce closures on the heap. Saving stack space isn't always more efficient.
This style opens up some useful programming techniques; and there are ways to package up them so the resulting code is both more powerful and easier to follow than direct-style programming. This is the purpose of this article.
Write a function in the continuation-passing style to compute x⁴ + 2x².
Write a main program to read a number from stdin, use
square_cps2 to compute the answer, and print the answer to
stdout. This exercise is about how to use a continuation-passing function in
a direct-style environment.
Define the following binary tree type, with numbers in the leaves:
data T = Leaf Integer | Tee T T
Write a recursive function in the continuation-passing style to sum the
numbers in such a tree. Use add_cps for adding. Use ordinary
pattern matching on the tree. Like this:
sumtree_cps :: T -> (Integer -> r) -> r sumtree_cps (Leaf n) = \k -> ... sumtree_cps (T lt rt) = \k -> ... (calls sumtree_cps for the subtrees) ...
Bi-continuation. Some functions take not just one continuation, but two. The idea is of conditional branching: The function decides which of the two continuations to send the answer to. The type looks like this:
f :: Parameters -> (X -> r) -> (Y -> r) -> r
The two continuations are the X->r parameter and the
Y->r parameter. X and Y could
be the same type or different types, depending on what f
does.
Write a function to take an Either parameter and two
continuations, and then: If it's a Left x, send x to
the 1st continuation; if it's a Right y, send y to
the 2nd continuation.
Write both the type and the code. Then compare with
Prelude.either.
The Cont monad packages up the continuation-passing style by a newtype wrapper and Monad methods. When combined with do-notation, the code can syntactically look like direct-style imperative code and not so mind-bending (until you do the really powerful things).
To understand this wrapping, recall one_cps from the
previous section (I just need its type for now):
one_cps :: (Integer -> r) -> r
We will wrap that type, except we would also like to generalize from Integer to a type variable. So we have two type variables overall. Here it goes:
newtype Cont r a = ContOf{unCont :: (a -> r) -> r}
-- Equivalent to, but different coding from, Cont from the transformers library
The reason for this order of type parameters—r first, a
last—is that the type of the answer, conceptually, is a. For example
one_cps gives you the answer 1, so conceptually its answer type is
Integer, not really r; r is there just because
one_cps is making your life difficult by insisting on the
continuation-passing style. But two difficults can make an easy by:
one :: Cont r Integer one = ContOf one_cps -- = ContOf (\k -> k 1)
Now you have a type saying it gives an Integer answer, even though the code does so by the continuation-passing style under the hood.
This idea of who's the answer type is justified by the fact that (Cont
r) makes a Monad instance. Using this fact and do-notation,
continuation-passing code can take a form easier to follow. Here is an example
showing how f_cps (which computes x²(x²+1))
is reborn this way:
mul, add :: Integer -> Integer -> Cont r Integer
mul x y = ContOf (mul_cps x y)
add x y = ContOf (add_cps x y)
f :: Integer -> Cont r Integer
f x = do
s <- mul x x
t <- add s 1
mul s t
(There will be an exercise on its equivalence to f_cps, once you
know how to define (>>=).)
This is easier to follow due to two factors. One factor is that you are no
longer bogged down in managing the user-provided continuation k—it is
taken care of by (>>=) behind the scene. (We will see how much
trouble we go through to implement it!) Another factor is that the do-notation
makes you think you're just calling procedures and using their return values,
rather than (the reality of) writing a lot of improvised lambdas. That second
factor could vanish in a puff of desugaring:
mul x x >>= \s -> add s 1 >>= \t -> mul s t
Still, it is so much nicer than manually plumbing k all the time.
I now walk you through how to implement the Monad methods twice, once by data flow, and once by types. There are lessons to learn from both perspectives.
The dataflow story of return: return 1 should do
what one above does. Generalizing, return x should be
sending x to the continuation, with a ContOf
wrapper:
return x = ContOf (\k -> k x)
The type story of return:
The overall type is a -> Cont r a, so we can begin with the
pretty easy template:
return x = ContOf (_ :: (a -> r) -> r) -- x :: a
A function is required. Let's be shallow and just try a lambda:
return x = ContOf (\k -> _ :: r) -- x :: a -- k :: a -> r
We now need to cough up a value of type r. Without knowing
what r is, but with x's and k's types
given, we can manage by k x:
return x = ContOf (\k -> k x)
The dataflow story of (>>=):
Begin with this template:
(ContOf a_cps) >>= arrb = ContOf (\k -> _) -- a_cps :: (a -> r) -> r, i.e., an unwrapped thing like one_cps.
The intended dataflow is this: We need to extract a_cps's
answer, give it to arrb. That in turn will lead to another
answer, which should be given to k. Then we're done.
To extract a_cps's answer, we give it an improvised
continuation:
(ContOf a_cps) >>= arrb = ContOf (\k -> a_cps (\a -> _))
Give the answer a to arrb:
(ContOf a_cps) >>= arrb = ContOf (\k -> a_cps (\a -> _ (arrb a) _))
Conceptually, (arrb a) holds the second answer and is
willing to give it, as soon as we specify a continuation; and we do
want k to be that continuation:
(ContOf a_cps) >>= arrb = ContOf (\k -> a_cps (\a -> _ (arrb a) k))
There is just one technicality: (arrb a) :: Cont r b,
we need to unwrap it to (b -> r) -> r before we can
pass k. The unwrapper is unCont.
(ContOf a_cps) >>= arrb = ContOf (\k -> a_cps (\a -> unCont (arrb a) k))
The type story of (>>=):
The overall type is
(>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
So begin with this template:
(ContOf a_cps) >>= arrb = ContOf (\k -> _ :: r) -- a_cps :: (a -> r) -> r -- arrb :: a -> Cont r b -- k :: b -> r
Now we need to cough up something of type r.
Two candidates may cough up r: a_cps (but we
have to write a function) or k (but we have to cough up
b). I start with a_cps:
(ContOf a_cps) >>= arrb = ContOf (\k -> a_cps (\a -> _ :: r)) -- a :: a -- arrb :: a -> Cont r b -- k :: b -> r
It is not too clear how to proceed, but the only way to make
a useful is to pass it to arrb:
(ContOf a_cps) >>= arrb = ContOf (\k -> a_cps (\a -> _ :: r)) -- arrb a :: Cont r b -- k :: b -> r
But that turns on a lightbulb: Cont r b is just an
unwrapping away from accepting k and coughing up a much awaited
value of type r:
(ContOf a_cps) >>= arrb = ContOf (\k -> a_cps (\a -> _ :: r)) -- unCont (arrb a) :: (b -> r) -> r -- k :: b -> r
So the final solution is:
(ContOf a_cps) >>= arrb = ContOf (\k -> a_cps (\a -> unCont (arrb a) k))
Remark: By starting with a_cps, I ended up solving this
outside-in. It is possible to start with k and solve this
inside-out, which I think is harder but don't let me stop you.
This finishes making instance Monad (Cont r), though without
proving that it satisfies the Monad laws. In the exercises, it will be your turn
to implement the Functor methods and the Applicative methods.
Technicality: Where you provide a Monad instance, the compiler will also insist on a Functor instance and an Applicative instance. If you haven't figured out how yet, and still want to use the compiler for other exercises, you can do this for now:
import Control.Monad(ap, liftM)
instance Functor (Cont r) where
fmap = liftM
instance Applicative (Cont r) where
pure = return
(<*>) = ap
There is an exercise below to explain the relevance of liftM and ap.
Rebirth squareplus1_cps as squareplus1 using
Cont and do-notation.
Rebirth sumtree_cps as sumtree using Cont and
do-notation.
Devise ways to test f, squareplus1, and
sumtree, in the daily direct-style environment.
Do algebra to show: unCont (squareplus1 x) = squareplus1_cps
x.
If that is too easy, also do algebra to show: unCont (f x) =
f_cps x.
Implement instance Functor (Cont r) and instance
Applicative (Cont r). Attempt both a dataflow story and a type
story.
If you are able to finish only one story, still use its solution to help discover the other story.
Failing even that, it is possible to jump between two partial stories and have them mutually help each other finish.
To get you started, here is how the top-level types can inform you of the dataflow story.
When you have a parameter of type like Cont r X, it
means that it holds an answer (of type X) you will want to
extract. To that end, it is a good idea to first unwrap to (X ->
r) -> r (by pattern matching or unCont) so you can
do continuation-passing style programming.
When you see the codomain Cont r b, it means that you
will want to fill in the template ContOf (\k -> _), in which
k is the user's continuation, and the blank is where you
write your dataflow story, culminating with sending the outcome (of type
b) to k.
(If the previous exercise is too easy:) Implement
join :: Cont r (Cont r a) -> Cont r a by dataflow and/or
by type.
It is possible to implement Functor and Applicative by just using their connections with Monad (true of all Monad instances):
fmap f xc = xc >>= \x -> return (f x) -- This is liftM. fc <*> xc = fc >>= \f -> xc >>= \x -> return (f x) -- This is ap.
Do algebra to show that these come down to your implementation.
(Oh, pure = return is too easy.)
Historical remark: The name “Applicative” is related to the name “ap”, and both means lifted function application.
(A lot of work with unclear benefit.) Prove that some or all of the Functor laws, the Applicative laws, and the Monad laws are satisfied.
So far what we have accomplished looks nice but roundabout: Learn how to convert direct-style code to the continuation-passing style, then learn how to use the Cont Monad to make it seem direct again. Not very worthwhile unless we also add something special, something out of line.
To understand what's out of line, it's useful to first review what's in
line. Observe that every time we have a continuation k, the only
thing we ever do is to call k exactly once with our answer. Sometimes
we do it right away, like ContOf (\k -> k x); other times it's a
subprogram that does it for us, for example ContOf (\k -> mul_cps x y
k).
What if we don't always call k exactly once with our answer?
What if we package up k in some form and leak it out? This is the subject of the next section Yield.
What if we call k multiple times, and with different answers? This is the subject of the section Quantifiers.
Before we embark on these journeys, it is useful to preview their common principle. They work by turning your code inside-out. More precisely, define:
run :: Cont R A -> R run cont_thing = unCont cont_thing fin -- fin is some function of type A -> R, depending on the application.
Then the following equation holds:
run (do a <- ContOf (\ka -> EXPR)
arrb a)
= let ka = \a -> run (arrb a)
in EXPR
where EXPR may use ka and may actually use it in an
out-of-line way. The equation is suggesting this: EXPR was an inner
expression, sitting in a larger context (run and the rest of the
do-block); but suddenly it becomes the outer expression, and the context becomes
an inner thing, available via ka so EXPR can leak it
out or use it several times or whatever. That is the inside-out I'm talking
about.
If this makes sense to you, great, proceed with the following journeys; if not, you will experience it more concretely in the applications, so proceed with the following journeys.
But here is the proof:
run (ContOf (\ka -> EXPR) >>= arrb) = run (ContOf (\k -> (\ka -> EXPR) (\a -> unCont (arrb a) k))) = unCont (ContOf (\k -> (\ka -> EXPR) (\a -> unCont (arrb a) k))) fin = (\ka -> EXPR) (\a -> unCont (arrb a) fin) = (\ka -> EXPR) (\a -> run (arrb a)) = let ka = \a -> run (arrb a) in EXPR
Prove
run (ContOf (\ka -> EXPR)) = let ka = fin in EXPR
Prove
run (ContOf (\kf -> EXPR) <*> xc) = let kf = \f -> run (fmap f xc) in EXPR
We are going to implement a yield command and a
toList command such that, for example,
toList (do yield 1
yield 2
return ())
= [1, 2]
= 1 : 2 : []
which looks really like Python's yield and generators. In fact, I'm pretty sure this is exactly what Python's yield and generators dream of (if only they are anthropomorphized) because generators are an OOP emulation of lazy lists. Well, Haskell lists are lazy lists.
To the end of conceiving how to do it, it seems that the intermediate steps would go like:
toList (do yield 1
yield 2
return ())
= 1 : toList (do yield 2
return ())
= 1 : 2 : toList (return ())
= 1 : 2 : []
toList is easier, so let's solve it first. The last step
suggests that toList is like run from the previous
section with fin = const []. So that's what we'll do, toList
prog = unCont prog (const []).
Now to solve yield. The first two steps should remind you of the
inside-out phenomenon in the last section. The yield command seems
to turn the whole block of code inside-out, itself becoming a list cons cell and
going outside, but also to leak out its continuation (the rest of the block) as
the list tail. This narrative suggests the following solution:
yield o = ContOf (\ka -> o : ka ???)
in which we still have to give a parameter to ka so that we get
a list rather than a naked function. While it's unclear what to give, it also
looks like no one is checking, so let's use ().
It is also valuable to re-tell the story with algebra. You want this to work in general:
toList (do _ <- yield o
more_stuff)
= x : toList (more_stuff)
With a little leap so we can use the inside-out equation from the last section:
= let ka = \_ -> toList (more_stuff)
in x : ka ???
= toList (do _ <- ContOf (\ka -> o : ka ???)
more_stuff)
which again suggests yield o = ContOf (\ka -> o : ka ???).
Putting it together, the overall solution:
toList prog = unCont prog (const []) toList :: Cont [o] unused -> [o] yield x = ContOf (\ka -> x : ka()) yield :: o -> Cont [o] ()
ObFibonacci: The following is probably the second least confusing code for the Fibonacci sequence in Haskell:
{-# LANGUAGE BangPatterns #-}
fibprog = loop 0 1
where
loop !m !n = do
yield m
loop n (m+n)
fibs = toList fibprog
(The Fibonacci sequence is everywhere in nature, for example Haskell tutorials and Python tutorials.)
In the remainder of this section, we extend the yielding mechanism so that a dialogue can be held between the producer and the consumer, and the producer can emit a final parting thought when it ends.
This extension is best understood by first beefing up the list type on the consumer side. Recall that the list type goes like:
-- Mock code, not finalized. data L o = Nil | Cons o (L o)
Adding a parting thought is easy: Instead of ending with the 0-ary
Nil, the end can have a field for the parting thought:
-- Mock code, not finalized. data L o r = Nil r | Cons o (L o)
Now, the reason this is a monologue from the producer is that in the Cons case, you have no way to contribute feedback to affect the tail of the list, you can only take it or leave it. For the tail to depend on your feedback, you need it to be a function:
-- Mock code, not finalized. data L i o r = Nil r | Cons o (i -> L o)
That does it. But I just want to rename it as it is named in the paper Yield: mainstream delimited continuations by Roshan P. James and Amr Sabry.
data Iterator i o r = Result r | Susp o (i -> Iterator i o r)
If you're wondering if this is a free monad, YES! But I won't make use of this fact.
That finishes extending the consumer side. The producer side is accordingly extended by:
toIterator prog = unCont prog Result toIterator :: Cont (Iterator i o r) r -> Iterator i o r yieldGet o = ContOf (\ki -> Susp o ki) yieldGet :: o -> Cont (Iterator i o r) i
Just like the story for toList and yield, the
solution for toIterator comes from desiring:
toIterator (return r) = Result r
so basically Result replaces const []. For
yieldGet we want it to come outside as a Susp cell,
and also to leak out its continuation as the second field. Except this time a
naked function is just right, since that's how the consumer can pass in
feedback. Formally, we want:
toIterator (i <- yieldGet o
more_stuff i)
= Susp o (\i -> toIterator (more_stuff i))
= let ki = \i -> toIterator (more_stuff i)
in Susp o ki
= toIterator (i <- ContOf (\ki -> Susp o ki)
more_stuff i)
An example toy application is the Fibonacci sequence again, except after yielding an item, the consumer can request going backward instead of forward. But if you go backward beyong the beginning, the producer ends.
{-# LANGUAGE BangPatterns #-}
data Direction = Forward | Backward
fibDirected = loop 0 1
where
loop _ 0 = return ()
loop !m !n = do
dir <- yieldGet m
case dir of
Forward -> loop n (m+n)
Backward -> loop (n-m) m
main = mainloop (toIterator fibDirected)
where
mainloop (Result _) = putStrLn "Brick wall."
mainloop (Susp o k) = do
print o
inp <- getLine
mainloop (k (if null inp then Forward else Backward))
In this example, there is not much informative parting thought the
producer can give when it ends, so it uses the boring ().
In the exercises, it will be your turn to write producers that implement
game masters or game AI's of simple games, in which case the parting thought
is meanginfully YouWin or YouLose.
ObFizzBuzz: Use toList and yield to produce the
Fizz Buzz sequence.
Since some items are numbers and some others are “Fizz” and/or “Buzz”, you may like to define your own algebraic data type for the items, or resort to making them all strings.
Use toList and yield to serialize a binary tree
pre-order, in-order, and post-order. More specifically, given the following
binary tree type with numbers in the internal nodes:
data BinTree = Nil | Node Integer BinTree BinTree
write three functions that take such a tree as parameter and yield the numbers in the tree, in pre-order, in-order, and post-order, respectively.
To experience the inside-out phenomenon first-hand, get your hands dirty in doing algebra to expand and simplify
toList (yield 1 >>= \_ -> yield 2)
to see how it evolves to 1 : 2 : [].
Use toIterator and yieldGet to serialize one
path in a binary tree, where the path is chosen by consumer feedback. More
specifically: Given this binary tree type again:
data BinTree = Nil | Node Integer BinTree BinTree
the producer starts by yielding the number at the root. Subsequently, at
each step the consumer dictates whether to go left or go right by calling
the leaked continuation (the 2nd field of Susp) with:
data LeftRight = Left | Right
(When the producer hits Nil, just return
().)
When I was a teenager, I was greatly fascinated by an animal-guessing program that came with the Apple II computer written in BASIC. This is actually much less ambitious than it sounds. In reality the computer just needed to ask some preloaded questions to the human, the human could only reply yes/no, and the computer would conclude with its guess, and it would be only one of the preloaded animal names.
Re-live those glorious old days (except the part about BASIC) by coding
up the computer's role with toIterator, yieldGet,
and your own decision tree of animals and yes/no questions. Add a
main to interact with the human player (or really you can only
be sure it's stdio). Take hint that there is a reason I put this
question right after the previous one.
Extra credit for getting it to run on an Apple II or a Commodore 64.
Choose a simple game and implement the game logic (if one-player game)
and one player's strategy (if two-player game) with toIterator
and yieldGet. Add a main to play against a human
or stdio player.
The intended flow is that the producer calls yieldGet to
output its move and/or the latest game state, and the consumer (after
consulting the human player) calls the leaked continuation with the human's
move. When the game ends, the producer detects this and returns
whether the human player wins or loses, and possibly the final game state if
it's of interest; this information goes to the consumer via the
Result cell.
You may encounter the problem that the producer needs initial
configuration, possibly also the human player's initial move (for some
games), which are not catered for by yieldGet. These have to be
passed as function parameters to the producer.
Some suitable games: Nim, Tic Tac Toe, Mastermind, Eliza, maze exploration.
There is a question solved using continuations in linguistics. (It does seem that more linguists than computer scientists and programmers know lambda calculi and continuations.) The question is about sentences like “everyone loves Bob” in contrast to “Alice loves Bob”.
“Alice loves Bob” is pretty obviously parsed as “loves” being the root or
outer element and the two nouns being the children or inner element. Further
translation to a semantic model preserves this structure. If you allow me to use
predicate logic or Haskell for semantics, in predicate logic it's loves(Alice,
Bob), and in Haskell it's loves Alice Bob.
I am well aware that Haskell, for example, is yet another syntax with its semantics. What can I say, one person's syntax is another person's semantics.
But then “everyone loves Bob” doesn't fit. Grammatically “loves” is still outer, and “everyone” is inner. But semantic models uproot that, literally. The meaning is something like: Alice loves Bob, Bob loves Bob, Charles loves Bob, and Diana loves Bob (if these are all the persons we have in mind). Contrary to the parse tree, the meaning puts “loves” inside and the every-ness outside. Predicate logic and Haskell also require similar inversions:
all (\x -> loves x Bob) [Alice, Bob, Charles, Diana]It would be nice to explain or cater for this inversion by a more fundamental principle than just “yeah look for special keywords to trigger special surgeries”. If anything, we would like the very definition of “everyone” (and “someone”, “no one”, “all prime numbers”…) to contain this inversion, rather than outsourcing it to a meta-level processor.
Ah, but inversion is our business!
First we still need a minor surgery. This is to delimit how much of the text the every-ness applies to. We as humans do this implicitly in our heads, but to be more rigorous we should at least record our judgment. So “everyone loves Bob” may become this representation:
-- Mock code, not finalized scope (loves everyone Bob)
Then we would like the definition of everyone, when expanded, to
lead to the inversion:
-- Mock code, not finalized scope (loves everyone Bob) = all (\a -> scope (loves a Bob)) [Alice, Bob, Charles, Diana]
in which the everyone inside becomes a quantifier and domain
outside, and the context becomes the predicate inside. It is actually a good
idea to retain the scope marker—imagine if you saw “everyone loves
everyone” or “everyone loves someone”. Both the narrative and the algebra
suggest these definitions:
everyone = ContOf (\p -> all p [Alice, Bob, Charles, Diana]) everyone :: Cont Bool Person scope stmt = unCont stmt id scope :: Cont r r -> r
Note how everyone will use its continuation (as a predicate)
multiple times (or zero times if you give the empty list).
There is just one technicality. Because of the monadic type everyone ::
Cont Bool Person, we cannot just use it with loves and
Bob verbatim. We have to lift them:
scope ((liftA2 loves) everyone (pure Bob))
That does it.
Our technicality requiring lifting is because we're using a purely functional
language, in which commands that jump around manipulating contexts—very, very
effectful—must bear at least a Functor type like Cont. The
linguists did this with an imperative language as their semantic language, so
they really had simply scope (loves everyone Bob). The next section is on the exact mechanism, “shift/reset”,
that the linguists actually used.
Lastly, here is more code for your further exploration:
import Control.Applicative(liftA2) -- ... insert code for Cont and its Functor, Applicative, Monad instances ... data Person = Alice | Bob | Charles | Diana deriving (Bounded, Enum, Eq, Ord, Show) persons :: [Person] persons = [minBound .. maxBound] loves :: Person -> Person -> Bool loves = (<=) lovesA :: Applicative f => f Person -> f Person -> f Bool lovesA = liftA2 loves scope :: Cont r r -> r scope prog = unCont prog id everyone :: Cont Bool Person everyone = ContOf (\p -> all p persons) someone :: Cont Bool Person someone = ContOf (\p -> any p persons) example1 = scope (lovesA everyone (pure Bob)) example2 = scope (lovesA someone (pure Bob))
Prove:
scope (do b <- pure Bob
return (loves a b))
= loves a Bob
Use that to help prove:
scope (liftA2 loves everyone (pure Bob)) = all (\a -> loves a Bob) [Alice, Bob, Charles, Diana]
Translate these sentences:
Where you think there is an ambiguity, resolve it all ways and translate them all.
Shift/Reset is one of many kinds of delimited continuations. Grossly
speaking, the main idea of delimited continuations (all kinds) is that there is
a command for capturing the command's context (continuation), but there is also
a command for lexically delimiting how much is captured. The different kinds
differ in details; in the case of shift/reset, the capturing command is called
shift, the delimiting command is called reset, and the
specific behaviour is:
reset (... shift (\ka -> EXPR) ...)
→ reset (let ka = \a -> reset (... a ...)
in EXPR)
assuming that the shift there is to be processed now.
Shift/Reset is what the linguists actually used to solve the quantifier
problem in the previous section. They had
reset where I had scope, and they defined
everyone = shift (\p -> ∀x∈{Alice, Bob, Charles, Diana}. p x)
The shift/reset rule comes close to our inside-out equation if we set:
reset prog = unCont prog id reset :: Cont r r -> r shift = ContOf shift :: ((a -> r) -> r) -> Cont r a
There are still two differences, and I will try to explain them away in the
next few paragraphs. First difference: The shift/reset rule still has an outer
reset after processing shift, while our inside-out
equation does not. Second difference: The shift/reset rule may process a
shift in the middle (when evaluation order requires it), while our
inside-out equation always processes the shift or
ContOf at the head of the block. (For both differences, the short
explanation is that shift/reset is formulated in an imperative language.)
To explain the first difference: Commands like shift,
yieldGet, and everyone are effectful, in the sense
that yieldGet's return value depends on external input, and
everyone even “returns” multiple times (or sometimes not at all).
In the Haskell version, the presence (non-absence actually) of this effect is
marked by the Cont type, but this is not done in the imperative
version. Now, this effect should be encapsulated: The point of the outer
reset is there to delimit its reach, so that the whole thing is a
pure value again. The whole thing needs to be a pure value both before and after
processing the shift inside, i.e., after EXPR comes
outside. In the Haskell version, EXPR no longer bears the
Cont type, so we know it is pure; but in the imperative version,
the type fails to say this, in fact EXPR is allowed to be
effectful, so an extra reset is needed around it.
To explain the second difference: In the imperative version, without the
Cont type to stop you, you can write like f (shift g)
y, and the computer will first process shift g (then
y, then finally the f call); this means the current
shift to be processed can very well be in the middle of nowhere. In
the Haskell version, the Cont type as a Monad type forces you to
code sequentially by way of (>>=) or do-notation, for example
shift g >>= \x -> return (f x y) if you want the shift
to be processed first; this means the inside-out equation just needs to work on
the leading shift.
Express toList in terms of reset,
yield in terms of shift. (Use the Haskell version of
shift/reset.)
Express toIterator in terms of reset,
yieldGet in terms of shift. (Use the Haskell version
of shift/reset.)
I have more Haskell Notes and Examples