Difference between revisions of "Cont computations as questionanswering boxes"
Tomjaguarpaw (talk  contribs) (Deleting page that hasn't been edited for over 10 years) 
m (Reverted edits by Tomjaguarpaw (talk) to last revision by CaleGibbard) 

Line 1:  Line 1:  
+  == Basic idea and definitions == 

+  
+  The basic idea behind the Cont monad is that in place of values of type t, you work with functions of type (t > r) > r, where r is some "response" type. Breaking this down a bit, you can think of a function of type t > r as a question about a value of type t which has a response of type r  for a yes or no question, r might be Bool, for instance. Then a function of type (t > r) > r, is like a box which takes a question about a value of type t, and produces an answer from that question. 

+  
+  In Haskell syntax, we define a new datatype to wrap up this idea: 

+  
+  <haskell> 

+  newtype Cont r t = Cont ((t > r) > r) 

+   a value of type Cont r t is of the form Cont f, 

+   where f is a function of type (t > r) > r 

+  </haskell> 

+  
+  We'd also, for convenience, define a function: 

+  
+  <haskell> 

+  runCont (Cont f) q = f q 

+  </haskell> 

+  
+  Which, given a Cont computation and a question, basically asks the question to get a response. 

+  
+  The simplest way to make such a box is for the box to just hang on to a value of type t, and answer questions about it truthfully, by simply applying them to the value. (The fun will happen later, when we come up with more twisted ways to get answers.) 

+  
+  This is embodied in the continuation monad by the function: 

+  
+  <haskell> 

+  return :: t > Cont r t 

+   return takes a value of type t 

+   and produces a Cont computation of type t with response type r. 

+  return x = Cont (\q > q x) 

+   produce a Cont computation which given a question q, 

+   applies the question to the value x. 

+  </haskell> 

+  
+  (The notation (\x > ...) is a [[Lambda abstraction]].) 

+  
+  Now, given a computation of type (Cont r t), and a ''continuation'' which is a function taking a value of type t to some computation of type (Cont r s), we'd like to have a way to join them together, producing a computation of type (Cont r s). That's a bit brain twisting, so let's think about how we might do it... 

+  
+  We're constructing a box which is going to receive a question q about a value of type s, and has to answer it somehow. 

+  
+  We have a box, which we'll call x, which answers questions about a value of type t. 

+  
+  We also have a function, f, which given a value of type t, will give a box which answers a question about a value of type s. 

+  
+  So what do we do? We ask x the question "if f were applied to your value v of type t, how would the resulting box respond to the question q?" 

+  
+  The operation which does this funny gluing together is called <code>>>=</code> (pronounced bind), and is implemented like this: 

+  
+  <haskell> 

+  (>>=) :: Cont r t > (t > Cont r s) > Cont r s 

+  x >>= f = Cont (\q > runCont x (\v > runCont (f v) q)) 

+  </haskell> 

+  
+  So we have what is effectively a fancy version of function application, which instead of working with straightforward values, works with these funky boxes that answer questions about values of the appropriate type. 

+  
+  == Laws == 

+  
+  There are three things which are true of the operations we've defined so far: 

+  
+  * <code>return v >>= f</code> is the same as <code>f v</code> 

+  * <code>x >>= return</code> is the same as <code>x</code> 

+  * <code>(x >>= f) >>= g</code> is the same as <code>x >>= (\v > f v >>= g)</code> 

+  
+  You might want to try to verify them as an exercise. These are the three monad laws, which makes <code>Cont r</code> a monad for any given response type r. 

+  
+  == Being sneaky: manipulating questions and responses == 

+  
+  With only these operations, things are rather boring. The first and second rules above basically tell us that anything we can express just in terms of <code>>>=</code> and <code>return</code>, we can also express without. 

+  
+  However, by working with black boxes that answer questions about values of type t, rather than values of type t directly, the boxes we construct can take steps to manipulate the question or response. 

+  
+  Given any function f which turns a question about a value of type s into a question about a value of type t, we can turn a box x which answers questions about a value of type t into a box which answers questions about a value of type s. In code: 

+  
+  <haskell> 

+  withCont :: ((s > r) > (t > r)) > Cont r t > Cont r s 

+  withCont f x = Cont (runCont x . f) 

+  </haskell> 

+  
+  That is, simply apply the function to the question first, and then ask x how it would answer. 

+  
+  Furthermore, given any function (r > r), which transforms responses somehow, and any box x, we can easily construct a box which asks the box x how it would respond to a question, and then transforms the response. 

+  
+  <haskell> 

+  mapCont :: (r > r) > Cont r t > Cont r t 

+  mapCont f x = Cont (f . runCont x) 

+  </haskell> 

+  
+  You certainly can't do either of these things with plain values! For example, let's consider the value <code>mapCont not (return 0) :: Cont Bool Integer</code>. It is a box that gives the opposite response to any True/False question that one would get if one asked the same question about the number 0. For example, we might do something like: 

+  
+  <haskell> 

+  ghci> runCont (mapCont not (return 0) >>= \t > return (t < 0 && t > 0)) id 

+  True 

+  </haskell> 

+  
+  The value 't' in the above is apparently a number which gives the appearance of simultaneously being both less than and greater than 0! Of course, what's really happening is that the test is turning out False and being negated after. 

+  
+  == Being sneakier: Making the result depend directly on the question == 

+  
+  There's an interesting insight to be had in thinking about the question that the computation <code>x</code> is given in the application <code>x >>= f</code>. 

+  
+  The question which x receives involves f, the computation which conceptually 'follows' after x is finished deciding on what value to supply to it. Can a carefullyconstructed x somehow sneakily manage to recover the function f from that question, and use it in determining what value it will then supply to that question? 

+  
+  The answer is that effectively, yes, it can. 

+  
+  <haskell> 

+  callCC :: ((t > Cont r s) > Cont r t) > Cont r t 

+  callCC g = Cont (\q > runCont (g (\v > Cont (\_ > q v))) q) 

+  </haskell> 

+  
+  TODO: Finish the explanation of what this means in terms of the question/answer approach. 
Latest revision as of 15:18, 6 February 2021
Contents
Basic idea and definitions
The basic idea behind the Cont monad is that in place of values of type t, you work with functions of type (t > r) > r, where r is some "response" type. Breaking this down a bit, you can think of a function of type t > r as a question about a value of type t which has a response of type r  for a yes or no question, r might be Bool, for instance. Then a function of type (t > r) > r, is like a box which takes a question about a value of type t, and produces an answer from that question.
In Haskell syntax, we define a new datatype to wrap up this idea:
newtype Cont r t = Cont ((t > r) > r)
 a value of type Cont r t is of the form Cont f,
 where f is a function of type (t > r) > r
We'd also, for convenience, define a function:
runCont (Cont f) q = f q
Which, given a Cont computation and a question, basically asks the question to get a response.
The simplest way to make such a box is for the box to just hang on to a value of type t, and answer questions about it truthfully, by simply applying them to the value. (The fun will happen later, when we come up with more twisted ways to get answers.)
This is embodied in the continuation monad by the function:
return :: t > Cont r t
 return takes a value of type t
 and produces a Cont computation of type t with response type r.
return x = Cont (\q > q x)
 produce a Cont computation which given a question q,
 applies the question to the value x.
(The notation (\x > ...) is a Lambda abstraction.)
Now, given a computation of type (Cont r t), and a continuation which is a function taking a value of type t to some computation of type (Cont r s), we'd like to have a way to join them together, producing a computation of type (Cont r s). That's a bit brain twisting, so let's think about how we might do it...
We're constructing a box which is going to receive a question q about a value of type s, and has to answer it somehow.
We have a box, which we'll call x, which answers questions about a value of type t.
We also have a function, f, which given a value of type t, will give a box which answers a question about a value of type s.
So what do we do? We ask x the question "if f were applied to your value v of type t, how would the resulting box respond to the question q?"
The operation which does this funny gluing together is called >>=
(pronounced bind), and is implemented like this:
(>>=) :: Cont r t > (t > Cont r s) > Cont r s
x >>= f = Cont (\q > runCont x (\v > runCont (f v) q))
So we have what is effectively a fancy version of function application, which instead of working with straightforward values, works with these funky boxes that answer questions about values of the appropriate type.
Laws
There are three things which are true of the operations we've defined so far:

return v >>= f
is the same asf v

x >>= return
is the same asx

(x >>= f) >>= g
is the same asx >>= (\v > f v >>= g)
You might want to try to verify them as an exercise. These are the three monad laws, which makes Cont r
a monad for any given response type r.
Being sneaky: manipulating questions and responses
With only these operations, things are rather boring. The first and second rules above basically tell us that anything we can express just in terms of >>=
and return
, we can also express without.
However, by working with black boxes that answer questions about values of type t, rather than values of type t directly, the boxes we construct can take steps to manipulate the question or response.
Given any function f which turns a question about a value of type s into a question about a value of type t, we can turn a box x which answers questions about a value of type t into a box which answers questions about a value of type s. In code:
withCont :: ((s > r) > (t > r)) > Cont r t > Cont r s
withCont f x = Cont (runCont x . f)
That is, simply apply the function to the question first, and then ask x how it would answer.
Furthermore, given any function (r > r), which transforms responses somehow, and any box x, we can easily construct a box which asks the box x how it would respond to a question, and then transforms the response.
mapCont :: (r > r) > Cont r t > Cont r t
mapCont f x = Cont (f . runCont x)
You certainly can't do either of these things with plain values! For example, let's consider the value mapCont not (return 0) :: Cont Bool Integer
. It is a box that gives the opposite response to any True/False question that one would get if one asked the same question about the number 0. For example, we might do something like:
ghci> runCont (mapCont not (return 0) >>= \t > return (t < 0 && t > 0)) id
True
The value 't' in the above is apparently a number which gives the appearance of simultaneously being both less than and greater than 0! Of course, what's really happening is that the test is turning out False and being negated after.
Being sneakier: Making the result depend directly on the question
There's an interesting insight to be had in thinking about the question that the computation x
is given in the application x >>= f
.
The question which x receives involves f, the computation which conceptually 'follows' after x is finished deciding on what value to supply to it. Can a carefullyconstructed x somehow sneakily manage to recover the function f from that question, and use it in determining what value it will then supply to that question?
The answer is that effectively, yes, it can.
callCC :: ((t > Cont r s) > Cont r t) > Cont r t
callCC g = Cont (\q > runCont (g (\v > Cont (\_ > q v))) q)
TODO: Finish the explanation of what this means in terms of the question/answer approach.