haskell - 如果“任一个”可以是“左”或“右”，但不能同时是“左”或“右”，那么为什么在Curry-Howard对应中它对应于OR而不是XOR？

Question

当我问this question时，答案之一(现已删除)建议Either类型对应Curry-Howard correspondence中的XOR而不是OR，因为它不能同时是Left和Right。
真相在哪里？

Answer 1

混淆源于逻辑的 bool 真值表说明。特别是，当两个参数均为True时，OR为True，而XOR为False。从逻辑上讲，这意味着证明“或”就足以提供其中一个论点的证明。但是如果另一个也为True也可以-我们不在乎。
在Curry-Howard解释中，如果有人给您提供了Either a b的元素，并且您能够从中提取a的值，则您仍然对b一无所知。它可能有人居住，也可能没有人居住。
另一方面，要证明XOR，您不仅需要一个参数的证明，还必须提供另一个参数的虚假证明。
因此，使用Curry-Howard解释，如果有人给您Xor a b元素，并且您能够从其中提取a的值，则可以得出结论b是无人居住的(即，与Void同构)。相反，如果您能够提取b的值，那么您将知道a是无人居住的。a的虚假证明是一个函数a->Void。给定Void的值，该函数将能够产生a的值，这显然是不可能的。因此，不能有a的值。 (只有一个函数返回Void，这就是Void上的标识。)