How come that we can implement call/cc, but the classical logic (intuitionistic + call/cc) is not constructive?

Question

Intuitionistic logic, being constructive, is the basis for type systems in functional programming. The classical logic is not constructive, in particular the law of excluded middle A ∨ ¬A (or its equivalents, such as double negation elimination or Pierce's law).

However, we can implement (construct) the call-with-current-continuation operator (AKA call/cc), for example as in Scheme. So why isn't call/cc constructive?

Tyndareus

Hm, we indeed can't implement call/cc in Scheme itself...It must be implemented from the runtime system, which has direct control over the stack. – Vaasta

Answer 1

The problem is that with call/cc the result depends on the order of evaluation. Consider the following example in Haskell. Assuming we have the call/cc operator

callcc :: ((a -> b) -> a) -> a
callcc = undefined

let's define

example :: Int
example =
    callcc (\s ->
        callcc (\t ->
            s 3 + t 4
        )
    )

Both functions are pure, so the value of example should be uniquely determined. However, it depends on the evaluation order. If s 3 is evaluated first, the result is 3; if t 4 is evaluated first, the result is 4.

This corresponds to two distinct examples in the continuation monad (which enforces order):

-- the result is 3
example1 :: (MonadCont m) => m Int
example1 =
    callCC (\s ->
        callCC (\t -> do
            x <- s 3
            y <- t 4
            return (x + y)
        )
    )

-- the result is 4
example2 :: (MonadCont m) => m Int
example2 =
    callCC (\s ->
        callCC (\t -> do
            y <- t 4 -- switched order
            x <- s 3
            return (x + y)
        )
    )

It even depends on if a term is evaluated at all or not:

example' :: Int
example' = callcc (\s -> const 1 (s 2))

If s 2 gets evaluated, the result is 2, otherwise 1.

This means that the Church-Rosser theorem doesn't hold in the presence of call/cc. In particular, terms no longer have unique normal forms.

Perhaps one possibility would be to view call/cc as a non-deterministic (non-constructive) operator that combines all the possible results obtained by (not) evaluating different sub-terms in various order. The result of a program would then be the set of all such possible normal forms. However the standard call/cc implementation will always pick just one of them (depending on its particular evaluation order).

Tyndareus

I think the type signature corresponding to the law of excluded middle should be callcc :: ((a -> Void) -> Void) -> a – Rainer