为什么我们可以实现 call/cc，但经典逻辑（直觉 + call/cc）却没有建设性？

Question

具有建设性的直觉逻辑是函数式编程中类型系统的基础。经典逻辑不具有建设性，尤其是排中律A ∨ ¬A（或其等价物，例如double negation elimination 或Pierce's law）。

但是，我们可以实现（构造）call-with-current-continuation 运算符（AKA call/cc），例如 Scheme。那么为什么 call/cc 没有建设性呢？

Answer 1

问题在于 call/cc 的结果取决于评估的顺序。考虑一下 Haskell 中的以下示例。假设我们有 call/cc 运算符

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

让我们定义

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

这两个函数都是纯函数，所以example 的值应该是唯一确定的。但是，这取决于评估顺序。如果先评估s 3，则结果为3；如果先评估t 4，则结果为4。

这对应于延续单子（强制执行顺序）中的两个不同示例：

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

它甚至取决于一个术语是否被评估：

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

如果s 2 被评估，则结果为2，否则为1。

这意味着 call/cc 存在时 Church-Rosser theorem 不成立。特别是，术语不再具有唯一的normal forms。

也许一种可能性是将 call/cc 视为一个非确定性（非构造性）运算符，它结合了通过（不）以各种顺序评估不同子项获得的所有可能结果.那么程序的结果将是所有这些可能的范式的集合。然而，标准的 call/cc 实现将始终只选择其中一个（取决于其特定的评估顺序）。