haskell - 有没有办法实现((a -> b) -> b) -> Either a b 类型的函数？

Question

建议 (P -> Q) -> Q和 P \/ Q是等价的。

有没有办法在 Haskell 中见证这种等价性:

from :: Either a b -> ((a -> b) -> b)
from x = case x of
         Left a -> \f -> f a
         Right b -> \f -> b

to :: ((a -> b) -> b) -> Either a b
to = ???

这样
from . to = id和 to . from = id ?

Answer 1

Propositions (P -> Q) -> Q and P \/ Q are equivalent.

这在经典逻辑中是正确的，但在构造逻辑中却不是。

在 build 性逻辑中，我们没有 law of excluded middle ，即我们不能从“P 为真或 P 不为真”开始思考。

经典地，我们的推理如下:

如果 P 为真(即我们有 (x :: P))，则返回 Left x .

如果 P 是假的，那么在 Haskell 中我们将有 nx :: P -> Void功能。然后absurd . nx :: P -> Q (我们可以使用任何类型的峰值，我们采用 Q )并调用给定的 f :: (P -> Q) -> Q)与 absurd . nx获取 Q 类型的值.

问题是，没有一个类型的一般功能:

lem :: forall p. Either p (p -> Void)

对于某些具体类型，例如 Bool有人居住所以我们可以写

lemBool :: Either Bool (Bool -> Void)
lemBool = Left True -- arbitrary choice

但是，总的来说，我们不能。