如果 Either 可以是 Left 或 Right 但不能同时是两者，那么为啥在 Curry-Howard 对应关系中它对应的是 OR 而不是 XOR？

Posted 2023-05-08

【中文标题】如果 Either 可以是 Left 或 Right 但不能同时是两者，那么为啥在 Curry-Howard 对应关系中它对应的是 OR 而不是 XOR？

【英文标题】：If Either can be either Left or Right but not both, then why does it correspond to OR instead of XOR in Curry-Howard correspondence?如果 Either 可以是 Left 或 Right 但不能同时是两者，那么为什么在 Curry-Howard 对应关系中它对应的是 OR 而不是 XOR？

【发布时间】：2021-01-31 06:58:12

【问题描述】：

当我问this question 时，现在已删除的答案之一是暗示Either 类型对应于Curry-Howard correspondence 中的XOR，而不是OR，因为它不能是Left 和@987654325 @同时。

真相在哪里？

【参考方案1】：

如果你有一个P 类型的值和一个Q 类型的值（也就是说，你有P 的证明和Q 的证明），那么您仍然可以提供Either P Q 类型的值。

考虑

x :: P
y :: Q
...

z :: Either P Q
z = Left x    -- Another possible proof would be `Right y`

虽然Either 没有明确表示这种情况的特定案例（与These 不同），但它没有做任何事情来排除它（如exclusive 或）。

两者都有证明的第三种情况与只有一个有证明的其他两种情况略有不同，这反映了直觉逻辑中“不排除”某事与“包含”某事有点不同的事实，因为Either 没有为此事实提供特定的证人。然而，Either 不是 XOR 通常工作的 XOR，因为正如我所说，它不排除两个部分都有证明的情况。另一方面，Daniel Wagner proposes in this answer 更接近 XOR。

Either 就其可能的见证人而言，有点像异或。另一方面，当您考虑是否可以在四种可能的情况下实际创建见证时，它就像 inclusive OR：拥有 P 的证明和 Q 的反驳，拥有Q 和 P 的反驳，同时证明或反驳两者。^[1] 当你有 P 和 Q 的证明时，你可以构造一个 Either P Q 类型的值（类似于包含 OR），您无法将此情况与只有 P 具有证明或只有 Q 具有仅使用类型为 Either P Q 的值的证明（有点类似于异或）的情况区分开来。另一方面，Daniel Wagner 的解决方案类似于构建和解构的异或。

还值得一提的是，These 更明确地表示两者都有证明的可能性。 These 类似于 inclusive OR 在构造和解构上。但是，还值得注意的是，当您同时拥有 P 和 Q 的证明时，没有什么可以阻止您使用“不正确”的构造函数。您可以扩展 These 以在这方面更能代表包容性 OR有点额外的复杂性：

data IOR a b
  = OnlyFirst  a       (Not b)
  | OnlySecond (Not a) b
  | Both       a       b

type Not a = a -> Void

如果您只对证明无关的逻辑系统感兴趣（意味着无法区分同一命题的任何两个证明），但在您希望逻辑中具有更多计算相关性的情况下，这可能很重要。^[2]

在编写实际要执行的计算机程序的实际情况中，计算相关性通常非常重要。尽管0 和23 都是Int 类型存在的证明，但总的来说，我们当然希望在程序中区分这两个值！

关于“建设”和“破坏”

本质上，我只是指通过构造“创建类型的值”和通过破坏“模式匹配”（有时人们在这里使用“引入”和“消除”这两个词，特别是在逻辑上下文中）。

以 Daniel Wagner 的解决方案为例：

构造：当你构造一个Xor A B 类型的值时，你必须提供一个恰好是A 或B 之一的证明，并反驳另一个。这类似于异或。不可能构造此值的，除非您对A 或B 有一个反驳并且另一个证据。一个特别重要的事实是，如果您同时拥有A 和B 的证明并且您不对它们中的任何一个都有驳斥（不像包括 OR）。

破坏：当您对Xor A B 类型的值进行模式匹配时，您总是拥有其中一种类型的证明和另一种类型的反驳。它永远不会为您提供两者的证明。这是从它的定义中得出的。

IOR的情况下：

构造：当您创建IOR A B 类型的值时，您必须执行以下操作之一：(1) 仅提供A 的证明和B 的反驳，（2）提供B的证明和B的反驳，（3）提供A和B的证明。这就像包容性 OR。这三种可能性与IOR 的三个构造函数中的每一个完全对应，没有重叠。请注意，与 These 的情况不同，在您同时拥有 A 和 B 的证明的情况下，您不能使用“不正确的构造函数”：在这种情况是使用Both（因为否则您需要提供A 或B 的反驳）。

破坏：由于您拥有A 和B 至少之一的证明的三种可能情况完全由IOR 表示，其中每个构造函数都有一个单独的构造函数（并且构造函数之间没有重叠），您将总是知道完全A 和B 中哪个为真，哪个为假（如果适用）通过对其进行模式匹配。

IOR 上的模式匹配

IOR 上的模式匹配与任何其他代数数据类型上的模式匹配完全相同。这是一个例子：

x :: IOR Char Int
x = Both 'c' 3

y :: IOR Char Void
y = OnlyFirst 'a' (\v -> v)

f :: Not p -> IOR p Int
f np = OnlySecond np 7

z :: IOR Void Int
z = f notVoid

g :: IOR p Int -> Int
g w =
  case w of
    OnlyFirst  p q -> -1
    OnlySecond p q -> q
    Both       p q -> q

-- We can show that the proposition represented by "Void" is indeed false:
notVoid :: Not Void
notVoid = \v -> v

然后是一个示例 GHCi 会话，加载了上面的代码：

ghci> g x
3
ghci> g z
7

---

^[1]当您认为某些陈述是不可判定的，因此您无法为它们构造证明或反驳时，这会变得有点复杂。

^[2]同伦类型理论将是证明相关系统的一个例子，但这已达到我目前知识的极限。

【讨论】：

大卫，我想我理解你的大部分回答；但是我仍然对您编写 Daniel Wagner 的解决方案的地方感到困惑，另一方面，在 construction 和 deconstruction 上都类似于异或；稍后您还提到了 在构造和解构中的包容性 OR。你能澄清一下这些部分吗？我想像“我可以声明这个值但不能声明这个”（就像你在第一段代码中所做的那样）这样的例子可能会帮助我理解你的观点。

另一件可能对我有帮助的事情是我将如何使用IOR。例如，我看到我可以对Both 进行模式匹配，因为Both a b = Both 3 'c' :: IOR Int Char 很好，并且符合我的预期。但是我将如何使用OnlyFirst？我可以对它进行模式匹配吗？这似乎与您提到的构造和解构有些相关，不是吗？

@Enrico 我在答案中添加了更多内容。这有帮助吗？

这当然有帮助。不过我想花点时间仔细看一下这三个答案，因为我还是不太清楚。

【参考方案2】：

也许尝试用“证据”替换 Curry-Howard 同构中的“证明”。

下面我将使用 斜体 表示命题和证明（我也将其称为证据），即同构的数学方面，我将使用 code 表示类型和值。

问题是：假设我知道P为真的[值对应]证据的类型（我将称这种类型为P），并且我知道Q 为真（我称这种类型为Q），那么命题的证据类型是什么R = P OR 问？

嗯，有两种方法可以证明R：我们可以证明P，或者我们可以证明Q。我们可以证明两者，但这将是不必要的工作。

现在问一下类型应该是什么？它是事物的类型，要么是 P 的证据，要么是 Q 的证据。 IE。值要么是 P 类型的东西，要么是 Q 类型的东西。 Either P Q 类型恰好包含这些值。

如果您有 P AND Q 的证据怎么办？那么这只是一个(P, Q)类型的值，我们可以写一个简单的函数：

f :: (p,q) -> Either p q
f (a,b) = Left a

如果我们可以证明 P AND Q，这给了我们一种证明 P OR Q 的方法。所以Either不能对应异或。

---

P XOR Q的类型是什么？

在这一点上，我会说，在这种建设性逻辑中，否定有点烦人。

让我们将问题转换为我们理解的东西，以及我们不理解的更简单的东西：

P XOR Q = (P AND (NOT Q)) 或 (Q AND (NOT P))

现在问：NOT P的证据类型是什么？

我没有直观的解释为什么这是最简单的类型，但如果不是 P 为真，那么 P 为真的证据将是矛盾的，这我们说证明 FALSE，即无法证明的事情（又名 BOTTOM 或 BOT）。也就是说，NOT P 可以写成更简单的术语：P IMPLIES FALSE。 FALSE 的类型称为 Void（在 haskell 中）。这是一种没有价值的类型，因为没有证据。因此，如果您可以构造该类型的值，您将遇到问题。 IMPLIES 对应于函数，因此对应于 NOT P 的类型是 P -> Void。

我们将它与我们所知道的相结合，并在命题语言中得到以下等价：

P XOR Q = (P AND (NOT Q)) 或 (Q AND (NOT P)) = (P AND (Q 暗示错误)) OR ((P 暗示错误）和Q）

那么类型是：

type Xor p q = Either (p, q -> Void) (p -> Void, q)

【讨论】：

我一直在关注你，但你在 我没有..., :/

是的，我认为在逻辑中引入 FALSE（即 BOT）是不直观的。也许将其视为矛盾。如果你能证明一些矛盾，你就可以证明任何事情（因为对于任何 P 都意味着 FALSE IMPLIES P）。因此，证明 NOT P 意味着如果它是真的，你就会有矛盾。

值得一提的是，您提到的矛盾属性称为the principle of explosion，有时也称为“ex falso quodlibet”。另外，顺便说一句，Void 与forall a. a 同构（没有真正提出特定的观点，只是认为这通常很有用）。

【参考方案3】：

混淆源于逻辑的布尔真值表阐述。特别是，当两个参数都为 True 时，OR 为 True，而 XOR 为 False。从逻辑上讲，这意味着证明 OR 足以证明其中一个论点；但如果另一个也是 True 也没关系——我们不在乎。

在 Curry-Howard 的解释中，如果有人给你一个 Either a b 的元素，并且你能够从中提取出 a 的值，那么你仍然对 b 一无所知。它可以有人居住，也可以不有人居住。

另一方面，要证明异或，你不仅需要证明一个论点，还必须提供另一个论点的虚假证明。

因此，根据 Curry-Howard 的解释，如果有人给你一个 Xor a b 的元素并且你能够从中提取 a 的值，你会得出结论 b 是无人居住的（即同构到Void)。相反，如果您能够提取b 的值，那么您就会知道a 是无人居住的。

a 的虚假证明是一个函数a->Void。给定a 的值，这样的函数将能够产生Void 的值，这显然是不可能的。所以不能有a 的值。 （只有一个函数返回Void，那就是Void上的身份。）

【讨论】：

对我来说，你答案的关键是它的最后一句话。谢谢你说，其他人没有。没有人费心去陈述显而易见的事情，但对于新学习者来说，显而易见的是根本不知道的事情。我一直试图找到这样的函数（除了undefined），但关键是它不存在。这意味着例如XOR Char Int 值也不存在。现在很清楚所有这些东西是关于什么的。总是说显而易见的！再次感谢。 ---- 所以，说a -> Void 存在与说a ~ Void 是一样的。 （在（“简单”？）Haskell）中可能没有其他方式来表达它。对吗？

@WillNess，而不是 Haskell 意义上的 ~。 Void 对于唯一同构是唯一的。 f :: XOR Char Int -> Void 存在，并且是唯一的。 absurd 是它唯一的逆。

@dfeuer 根据 Bartosz 的回答，f = id。所以这一定意味着XOR Char Int 与Void 统一？

@WillNess，我认为他的写作有点松散。

@WillNess，是的。有很多空类型，它们都以最无聊的方式等价（同构）（每对之间只有一个同构）。这是范畴论中初始对象的一般性质。让V1 和V2 成为初始对象。通过init obj的def，有唯一的f :: V1 -> V2，g :: V2 -> V1。 f . g :: V2 -> V2 和 g . f :: V1 -> V1。通过唯一性，f . g = id_V2 和 g . f = id_V1。为什么 Hask 中的空类型是初始对象？当两个函数都不能被实际调用时，这两个函数之间就没有有意义的区别。