有没有一种方法可以实现类型为（（a-> b）-> b）-> ab的函数？

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

命题(P -> Q) -> Q和P \/ Q是等价的。

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

在构造逻辑中，我们没有排除中间定律，即我们不能以“ P为真或P不为真”开始思考。

传统上，我们的推理如下：

• 如果P为true（即，我们有（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

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

Answer 2

不，这是不可能的。考虑以下特殊情况Q = Void。

Either P Q然后是Either P Void，与的同构P。

iso :: P -> Either P Void
iso = Left

iso_inv :: Either P Void -> P
iso_inv (Left p)  = p
iso_inv (Right q) = absurd q

因此，如果我们有一个功能项

impossible :: ((P -> Void) -> Void) -> Either P Void

我们也可以有一个学期

impossible2 :: ((P -> Void) -> Void) -> P
impossible2 = iso_inv . impossible

根据Curry-Howard的对应关系，这将是直觉逻辑中的重言式：

((P -> False) -> False) -> P

但是以上是双重否定消除，众所周知，在直觉逻辑中不可能证明这是矛盾的。（我们可以用经典逻辑证明这一事实是不相关的。）

（最后的注：这假设Haskell程序终止了。当然，使用无限递归undefined和类似的方法实际上避免返回结果，我们可以在Haskell中使用任何类型。）

Answer 3

不，这是不可能的，但这有点微妙。问题在于类型变量a和b是普遍量化的。

to :: ((a -> b) -> b) -> Either a b
to f = ...

a并被b普遍量化。调用者选择它们的类型，因此您不能只创建任一类型的值。这意味着您不能只创建 type 的值Either a b而忽略 argument f。但使用f也是不可能的。如果不知道a和是什么类型，您就无法创建要传递给b的类型值。当类型被普遍量化时，没有足够的信息可用。a -> bf

至于为什么同构在 Haskell 中不起作用 - 你确定这些命题在构造性直觉主义逻辑中是等价的吗？Haskell 没有实现经典的演绎逻辑。