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

Question

当我问这个问题，其中一个答案，现在删除，是在暗示该类型Either对应于XOR，而不是OR，在柯里-霍华德同构的，因为它不能Left与Right在同一时间。

真相在哪里？

Answer 1

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

考虑

x :: P
y :: Q
...

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

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

两者都有证明的第三种情况与只有一个证明的其他两种情况略有不同，这反映了这样一个事实，即“不排除”某事与直觉逻辑中的“包括”某事有点不同，因为Either不提供这一事实的特别证人。然而Either，XOR 并不是 XOR 通常工作的方式，因为正如我所说，它不排除两个部分都有证明的情况。什么丹尼尔·瓦格纳在这个答案提出，在另一方面，是更接近的XOR。

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

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

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

type Not a = a -> Void

的潜在的“错误的构造”的问题These（以及缺乏在“两个”证人Either）其实并不重要，如果你只在无关紧要的证明逻辑系统感兴趣（意思是没有办法中的任意两个证据之间的区分相同的命题），但在您希望在逻辑中具有更多计算相关性的情况下可能很重要。^[2]

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

关于“建设”和“破坏”

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

在 Daniel Wagner 的解决方案中：

• 构造：当你构造一个 type 的值时Xor A B，你必须提供恰好一个Aor的证明B和另一个的反驳。这类似于异或。这是不可能建造的这个值，除非您有任何反驳A或B 与另一种证明。特别显著的事实是，你不能建立这种类型的值，如果你有两个证明A和B你不要有任何一方的反驳（不像含OR）。

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

在以下情况下IOR：

• 构造：创建 type 的值时IOR A B，您必须完全执行以下操作之一：(1) 仅提供 的证明A和反驳B，(2) 提供 的证明B和反驳B，(3) 提供证明两个A和B。这就像包含 OR。这三种可能性完全对应 的三个构造函数中的每一个IOR，没有重叠。需要注意的是，不同的形势These，你不能在你有两个证明的情况下使用了“不正确构造”A和B：只有这样，才能使类型的值，IOR 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]同伦类型理论将是证明相关系统的一个例子，但这已经达到了我目前知识的极限。

Answer 2

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

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

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

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

现在问应该是什么类型？它是作为P 的证据或Q 的证据的事物的类型。即值要么是类型的P东西要么是类型的东西Q。该类型Either P Q恰好包含这些值。

如果你有P AND Q 的证据怎么办？好吧，这只是一个 type 的值(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 )) OR ( Q AND (NOT P ))

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

我没有为什么，这是最简单的类型的直观的解释，但如果没有P是真正然后证据P为真会是一对矛盾，这是我们说的是假证明，在无法证明的东西（又名底部或BOT）。也就是说，NOT P可以用更简单的术语写成：P IMPLIES FALSE。FALSE 的类型称为Void（在 haskell 中）。它是一种没有值存在的类型，因为没有它的证明。因此，如果您可以构造该类型的值，您就会遇到问题。IMPLIES 对应于函数，因此对应于 NOT P的类型是P -> Void。

我们把它和我们所知道的放在一起，并在命题语言中得到以下等价：

P XOR Q = ( P AND (NOT Q )) OR ( Q AND (NOT P )) = ( P AND ( Q IMPLIES FALSE)) OR (( P IMPLIES FALSE) AND Q )

那么类型是：

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

Answer 3

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

在库里-霍华德的解释中，如果有人给你一个 的元素Either a b，而你能够从中提取出 的值a，你仍然对 一无所知b。它可能有人居住，也可能无人居住。

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

所以，根据库里-霍华德的解释，如果有人给你一个元素Xor a b并且你能够从中提取出 的值a，你会得出结论b是无人居住的（即同构于Void）。相反，如果您能够提取 的值b，那么您就会知道它a是无人居住的。

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