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

Posted 2023-05-08

【中文标题】有没有办法实现((a -> b) -> b) -> Either a b 类型的函数？

【英文标题】：Is there a way to realize a function of type ((a -> b) -> b) -> Either a b?

【发布时间】：2020-03-03 06:10:25

【问题描述】：

命题(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?

【问题讨论】：

在我看来这是不可能的，但也许我错了。如果是这样，一个有用的起点是具有完全多态类型((a -> b) -> b) 的函数与a 同构：唯一可能的实现是g f = f someHardcodedA。

@amalloy 还有另一种可能的实现方式：g = const someHardcodedB

啊，当然。它是a 或b。有道理。

如果 Haskell 有 call/cc，那么 to f = callcc (\k -> k (Right (f (\a -> k (Left a))))) 就可以了。 （这是隐含的有效经典证明。）

【参考方案1】：

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

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

在建设性逻辑中，我们没有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

但总的来说，我们不能。

【参考方案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 的对应关系，这将是 intuitionistic 逻辑中的重言式：

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

但以上是双重否定消除，众所周知，在直觉主义逻辑中是不可能证明的——因此是矛盾的。 （我们可以在 classical 逻辑中证明它的事实并不相关。）

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

【参考方案3】：

不，这是不可能的，但它有点微妙。问题是类型变量a 和b 是通用量化的。

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

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

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

【参考方案4】：

正如其他人指出的那样，这是不可能的，因为我们没有排中律。让我更明确地讨论一下。假设我们有

bogus :: ((a -> b) -> b) -> Either a b

我们设置b ~ Void。然后我们得到

-- chi calls this `impossible2`.
double_neg_elim :: ((a -> Void) -> Void) -> a
bouble_neg_elim f = case bogus f of
             Left a -> a
             Right v -> absurd v

现在，让我们证明排中律的双重否定应用于特定命题。

nnlem :: forall a. (Either a (a -> Void) -> Void) -> Void
nnlem f = not_not_a not_a
  where
    not_a :: a -> Void
    not_a = f . Left

    not_not_a :: (a -> Void) -> Void
    not_not_a = f . Right

现在

lem :: Either a (a -> Void)
lem = double_neg_elim nnlem

lem 显然不存在，因为a 可以编码我碰巧选择的任何图灵机配置都会停止的命题。

---

让我们验证lem 是否足够：

bogus :: forall a b. ((a -> b) -> b) -> Either a b
bogus f = case lem @a of
  Left a -> Left a
  Right na -> Right $ f (absurd . na)

【参考方案5】：

我不知道这在逻辑上是否有效，或者它对您的等效性意味着什么，但是可以在 Haskell 中编写这样的函数。

要构造Either a b，我们需要a 或b 值。我们没有任何方法可以构造一个a 值，但是我们确实有一个函数可以返回一个我们可以调用的b。为此，我们需要提供一个将a 转换为b 的函数，但鉴于类型未知，我们最多可以创建一个返回常量b 的函数。要获得 b 的值，我们不能以任何其他方式构造它，所以这变成了循环推理 - 我们可以通过简单地创建一个 fixpoint 来解决这个问题：

to :: ((a -> b) -> b) -> Either a b
to f = let x = f (\_ -> x) in Right x