No. This implementation of callcc
doesn't depend upon lazy evaluation. To prove this I'll implement it in a strict functional language and show that anything after k n
is not executed at all.
The strict functional language I'll be using is JavaScript. Since JavaScript is not statically typed you don't need to declare a newtype
. Hence we start by defining the return
and >>=
functions of the Cont
monad in JavaScript. We'll call these functions unit
and bind
respectively:
function unit(a) {
return function (k) {
return k(a);
};
}
function bind(m, k) {
return function (c) {
return m(function (a) {
return k(a)(c);
});
};
}
Next we define callcc
as follows:
function callcc(f) {
return function (c) {
return f(function (a) {
return function () {
return c(a);
};
})(c);
};
}
Now we can define quux
as follows:
var quux = callcc(function (k) {
var n = 5;
return bind(k(n), function () {
alert("Hello World!");
return unit(25);
});
});
Note that I added an alert
inside the second argument to bind
to test whether or not it's executed. Now if you call quux(alert)
it will display 5
but it won't display "Hello World!"
. This proves that the second argument to bind
was never executed. See the demo for yourself.
Why does this happen? Let's start backwards from quux(alert)
. By beta reduction it's equivalent to:
(function (k) {
var n = 5;
return bind(k(n), function () {
alert("Hello World!");
return unit(25);
});
})(function (a) {
return function () {
alert(a);
};
})(alert);
By beta reducing it again it becomes:
bind(function () {
alert(5);
}, function () {
alert("Hello World!");
return unit(25);
})(alert);
Next by the beta reduction of bind
we get:
(function (c) {
return (function () {
alert(5);
})(function (a) {
return (function () {
alert("Hello World!");
return unit(25);
})(a)(c);
});
})(alert);
Now we can see why "Hello World!"
was never displayed. By beta reduction we're executing function () { alert(5); }
. It's the job of this function to call its argument, but it never does. Because of this execution stops and "Hello World!"
is never displayed. In conclusion:
The callcc
function doesn't depend upon lazy evaluation.
The function created by callcc
terminates after k
is called not because of lazy evaluation but because calling k
breaks the chain by not calling it's first argument and hence returns immediately.
This brings me back to your question:
And we can see from the definition of
k
which is\a -> cont $ \_ -> h a
that in the above we have\x -> runCont ((\_ -> return 25) x) c
being passed into the argument that is ignored with underscore. Ultimately thereturn 25
is effectively "ignored" because the underscore argument is never used so from lazy evaluation its never evaluated.
You're mistaken. As you can see k
is (\a -> cont $ \_ -> h a)
and the function (\x -> runCont ((\_ -> return 25) x) c)
is passed into the the argument that's ignored by k
. You were correct until then. However this doesn't mean that return 25
is not evaluated because of lazy evaluation. It's simply not evaluated because the function (\x -> runCont ((\_ -> return 25) x) c)
is never called. I hope that cleared things up.