Why can we 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. Classical logic is not constructive, in particular the law of excluded mean A ∨ ¬A (or its equivalents, such as double negation or Pierce's Law ).

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

Answer 1

The problem is that when / cc is called, the result depends on the evaluation order. Consider the following example in Haskell. Assuming we have a call / cc operator

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

define

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

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

This corresponds to two different examples in the continuation of the monad (which provides 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 whether the term is evaluated at all or not:

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

If s 2 gets an estimate, the result is 2 , otherwise 1 .

This means that the Church-Rosser theorem does not contain, in the presence of the / cc call. In particular, the terms no longer have unique normal forms .

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