I couldn’t find a simple written explanation of callcc
, its type, and the connection to classical logic, so I thought I’d write one here.1 I won’t assume that you are familiar with the syntax of Scheme (because I’m not), so I will be using a made up language. I hope the first part of this post will be self-contained, so that you don’t have to understand any particular langauge to understand callcc
. The second part concerns how the type of callcc
relates to classical logic under
Curry-Howard Correspondence
. I will assume some familiarity and comfort with the concept and type theory notations.
Prelude: Syntax
The syntax we use here is close to functional programming languages like ML.
- Everything is an expression, so has a value.
- Function definition: A function that takes input
x
and returnz
is written as(fn x => z)
. All functions take only one argument. Besidescallcc
, any other function is anonymous. - Function application: To call a function
f
with argumentsx
, we writef x
(with space in-between). - Function type: A function
f
with argumentsx
has the type ifx
has type and the return value of has typeB
. Note thatx
or the return value could be functions, in which case we parenthesize the type accordingly. For example, ifx
is a function of type , thenf
has type . - When we write expressions in sequence,
e1; e2; ...; en
, the whole expression has the value ofen
.
There are other mischellaneous syntaxes like integer addition, which we won’t be focusing on. But they should be obvious.
Part 1: What is callcc
and its type?
callcc f
callcc (fn c => ...)
callcc
takes a function f
and returns a value. The function it takes, f
, takes another function c
. Such c
is what’s called the “current continutation”, which is “the rest of the computation” outside of callcc
. All this probably doesn’t make much sense, but don’t worry, we will see what this means in a bit.
To understand how callcc
works, we split uses of callcc
into two scenarios:
Scenario 1: If f
in callcc
returns a value directly without using c
, then the value is returned, and nothing special happens. Suppose we have the following code:
1 + callcc (fn c => 3)
To evaluate the operator +
, we evaluate 1
to be 1
, then we evaluate callcc
. Since it just returns 3
, the whole thing evaluates to 1 + 3 = 4
.
Scenario 2: If f
in callcc
calls the contituation function c
with some argument x
, then callcc
invokes the current continuation with x
. The rest of the code inside callcc
is discarded/aborted (even though they might have been evaluated), and we continue in the current continuation. What does “current continutation” means? An example would help:
1 + callcc (fn c => c 5)
You can treat current continuation as a function that wraps the outer code, and replaces callcc (fn c => ...)
with its argument. So here, the current continuation is fn x => 1 + x
. This becomes the argument c
to f
.
Again, let us walk through the evaluation. 1
is first evaluated, then we evaluate callcc
, which calls c 5
. Then the computation inside callcc is aborted, and the whole expression evaluates to 1 + 5 = 6
. Note that this value is not passed back to the outer context (the 1 + ...
) again, rather, the outer context c
is used inside callcc
.
What if we have more code in callcc
?
1 + callcc (fn c => 7 + 9; c 5; c 6)
Inside f
, expression sequences are evaluated left to right. First, 7+9
is evaluated. Then c 5
. As soon as c
is called, the computation inside f
ends, so c 6
is never evaluated. Since 1 + 5 = 6
, the whole expression evaluates to 6
.
So you can see that calling c
basically aborts the computation inside callcc
, and “returns the argument to c
as value to the outer context.”
Let us look at something stranger as our last example (Here, ^
is string concatenation):
"This is " ^ callcc (fn c => 1 + (c "strange"); "not strange")
Again, 1
is evaluated, and c "strange"
is as well, which evaluates the whole program to the string "This is strange"
. "not strange"
is never evaluated. Notice that we tried to add an integer with the result of c "strange"
; this is fine because c "strange"
will never return a value to be added!
So, what is the type of callcc
?
In either case (whether c
is used or not), it must return the same type that the outer context is expecting of it (in the first example, that would be an int
, because 1 + ...
expects an int
).
So if the outer context is expecting type
where “f
.
What is the type of f
? it must take some function c
, and return the same type as what callcc
returns. So the type of callcc
is:
where “c
.
What is the type of c
? We know it must take something of type c
is called, it will never return to inside the f
function. So it can be anything. Let’s give it another variable, Q
. So the type of callcc
becomes:
Part 2: Connection to Classical Logic
How does all this relate to classical logic? If you have heard of the Curry-Howard Correspondence , you know that in certain programming languages, the types of well-typed programs corresponds to theorems of some logic, and the programs corresponds to the proofs of the theorems.
It is well-known that a language with the function, product, and sum type corresponds to
intuitionistic (propositional) logic
. Here we set up the type theory for intuitionist logic briefly, then look at how callcc
can extend it so that well-typed programs corresponds to classical theorems.2
Type Theory and Intuitionist Logic
We outline below the connection between types and connectives, and provide rules that will be useful to us. The rules we give are typing rules, but their logical counterparts is identical except for each pairing
- The function type corresponds to implication. In other words, a function of type
transforms proofs of to proofs of . The lambda abstraction/application rule corresponds to the implication introduction/elimination rule, respectively.
-
The product type (type of pairs/
-tuples) corresponds to conjunction. We won’t talk much about conjunctions here. -
The sum type, written as
, is a type that is either or . This corresponds to disjunction.- In particular, the empty sum type, written as
, is a type that (should) have no inhabitant. - If there is an inhabitant of the empty sum type, then the program has gone wrong! We write this as the following rule, which corresponds to the
principle of explosion
, or ex falso quodlibet, in logic:
- In particular, the empty sum type, written as
-
Negation is defined as
.
For more information and examples on the Curry Howard correspondence, see my post here.
Getting Classical
There are certain propositions that are not theorems in intuitionist logic, but they are theorems in classical logic. The most famous examples are Law of Excluded Middle (LEM) and Double Negation Elimination (DNE):
- LEM
- DNE
They are quite magical: If we add LEM or DNE as axioms to intuitionistc logic, we can then prove everything we can prove in classical logic. In other words, intuitionist logic + LEM/DNE = classical logic.
There is, however, a less well-known proposition that is equivalent to the two above, which is Pierce’s law :
- Pierce’s law
This is exactly the type of callcc
!
This tells us that when our type theory is intuitionistic, we just need to add callcc
to get a type theory for classical logic. This makes sense, because if we let
You might not be convinced yet at this point, and that’s ok. Let us prove that Pierce’s law implies DNE.4 First, we give a purely logical proof (intuitionistically valid):
1. | Pierce’s law | |
2. | Assume for conditional proof | |
3. | Assume for conditional proof | |
4. | From 2 and 3 | |
5. | By explosion from 4 | |
6. | Conditional proof, 3 ~ 5 | |
7. | ||
8. | Conditional proof, 2 ~ 7 |
Then we give the program whose type is the proposition DNE, using callcc
:
This might seem a bit complicated at first, so I annotated relevant variables and expressions with their types. Here is the relation between the proof above and the program:
- corresponds to the premise that
callcc
is a well typed function - corresponds to binding
in the outer - corresponds to binding
in the inner - corresponds to the type of
- corresponds to using
for explosion - corresponds to the lambda abstraction of
- corresponds to the lambda application to
callcc
- corresponds to the lambda abstraction of
The whole program then has the type of DNE. Knowing the program representing the proof, one can easily rewrite the proof in the same style as the inference rules mentioned above. Since it would be a bit unreadable on this page, we leave it as an exercise to the reader.
-
In lambda calculus (the language we are using),
is a function that takes as input and returns , and is calling a function with as input (separated by space). So for example, returns . ↩︎ -
Each statement in a rule has the format
. In the type theory realm, it says that given the pairing of types to variables in the set , we can derive that has type . In the logic realm, it says that given the premises (types) in , we can derive the conclusion . Rules can be read in a top down manner: If statements above the line holds, then the statement below the line holds. ↩︎ -
We leave the reverse direction to the reader because it is unnecessary for our purposes, and we don’t have a concrete function whose type is DNE that we can use to construct a function whose type is Pierce’s law. ↩︎