Difference between revisions of "Cont computations as questionanswering boxes"
m (Reverted edits by Tomjaguarpaw (talk) to last revision by CaleGibbard) 
m (Various minor changes; category added.) 

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

−  The basic idea behind the Cont 
+  The basic idea behind the monadic <code>Cont</code> type is that in place of values of type <code>t</code>, you work with functions of type<br><code>(t > r) > r</code>, where <code>r</code> is some "response" type. Breaking this down a bit, you can think of a function of type <code>t > r</code> as a question about a value of type <code>t</code> which has a response of type <code>r</code>  for a ''yes''or''no'' question, <code>r</code> might be <code>Bool</code>, for instance. Then a function of type <code>(t > r) > r</code>, is like a box which takes a question about a value of type <code>t</code>, and produces an answer from that question. 
In Haskell syntax, we define a new datatype to wrap up this idea: 
In Haskell syntax, we define a new datatype to wrap up this idea: 

Line 17:  Line 17:  
</haskell> 
</haskell> 

−  Which, given a Cont computation and a question, basically asks the question to get a response. 
+  Which, given a <code>Cont</code> 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.) 
+  The simplest way to make such a box is for the box to just hang on to a value of type <code>t</code>, 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: 
This is embodied in the continuation monad by the function: 

Line 32:  Line 32:  
</haskell> 
</haskell> 

−  (The notation 
+  (The notation <code>\x > ...</code> is a [[lambda abstractionLambda abstraction]].) 
−  Now, given a computation of type 
+  Now, given a computation of type <code>Cont r t</code>, and a ''continuation'' which is a function taking a value of type <code>t</code> to some computation of type <code>Cont r s</code>, we'd like to have a way to join them together, producing a computation of type <code>Cont r s</code>. That's a bit braintwisting, 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're constructing a box which is going to receive a question <code>q</code> about a value of type <code>s</code>, 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 have a box, which we'll call <code>x</code>, which answers questions about a value of type <code>t</code>. 
−  We also have a function 
+  We also have a function <code>f</code> which given a value of type <code>t</code>, will give a box which answers a question about a value of type <code>s</code>. 
−  So what do we do? We ask x 
+  So what do we do? We ask <code>x</code> this question: ''if <code>f</code> were applied to your value <code>v</code> (of type <code>t</code>) how would the resulting box respond to the question <code>q</code>?'' 
−  The operation which does this funny gluing together is called <code>>>=</code> (pronounced bind), and is implemented like this: 
+  The operation which does this funny gluing together is called <code>(>>=)</code> (pronounced "bind"), and is implemented like this: 
<haskell> 
<haskell> 

Line 61:  Line 61:  
* <code>(x >>= f) >>= g</code> is the same as <code>x >>= (\v > f v >>= g)</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. 
+  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 <code>r</code>. 
== Being sneaky: manipulating questions and responses == 
== Being sneaky: manipulating questions and responses == 

Line 67:  Line 67:  
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. 
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. 
+  However, by working with black boxes that answer questions about values of type <code>t</code>, rather than values of type <code>t</code> 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: 
+  Given any function <code>f</code> which turns a question about a value of type <code>s</code> into a question about a value of type <code>t</code>, we can turn a box <code>x</code> which answers questions about a value of type <code>t</code> into a box which answers questions about a value of type <code>s</code>. In code: 
<haskell> 
<haskell> 

Line 76:  Line 76:  
</haskell> 
</haskell> 

−  That is, simply apply the function to the question first, 
+  That is, simply apply the function to the question first, then ask <code>x</code> how it would answer. 
−  Furthermore, given any function 
+  Furthermore, given any function <code>r > r</code>, which transforms responses somehow, and any box <code>x</code>, we can easily construct a box which asks the box <code>x</code> how it would respond to a question, and then transforms the response. More code: 
<haskell> 
<haskell> 

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

Line 92:  Line 92:  
</haskell> 
</haskell> 

−  The value 
+  The value <code>t</code> in the above example is apparently a number which gives the appearance of simultaneously being both less than and greater than <code>0</code>! Of course, what's really happening is that the test is turning out <code>False</code> and being negated after. 
== Being sneakier: Making the result depend directly on the question == 
== 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 
+  There's an interesting insight to be had in thinking about the question that the computation <code>x</code> is given in the application<br><code>x >>= f</code>. 
−  The question which x receives involves f, the computation which conceptually 
+  The question which <code>x</code> receives involves <code>f</code>, the computation which conceptually "follows" after <code>x</code> is finished deciding on what value to supply to it. Can a carefullyconstructed <code>x</code> somehow sneakily manage to recover the function <code>f</code> 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. 
The answer is that effectively, yes, it can. 

Line 107:  Line 107:  
</haskell> 
</haskell> 

−  TODO: Finish the explanation of what this means in terms of the question/answer approach. 
+  ''TODO: Finish the explanation of what this means in terms of the question/answer approach.'' 
+  
+  [[Category:Pages under construction]] 
Latest revision as of 23:34, 25 June 2021
Contents
Basic idea and definitions
The basic idea behind the monadic Cont
type 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 yesorno 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 braintwisting, 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
this 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, 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. More code:
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 example 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 applicationx >>= 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.