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

callcc, continuations, curry-howard, functional-programming

Solution

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).

Problem

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?

Original source