在类型理论中，什么类型对应于a xor b？

Question

在范畴论 8.2结束时，Bartosz Milewski展示了逻辑、范畴论和类型系统之间的一些对应实例。

我想知道逻辑异或运算符对应的是什么。我知道

a xor b == (a ∨ b) ∧ ¬(a ∧ b) == (a ∨ b) ∧ (¬a ∨ ¬b)

所以我只解决了问题的一部分：a xor b 对应于 (Either a b, Either ? ?)。但是缺失的两种类型是什么？

看起来如何编写xor实际上归结为如何编写not。

那么¬a是什么？我的理解是，如果存在至少一个类型为a的元素，则a为逻辑真。因此，对于not a为真，a应该是假的，即它应该是Void。因此，在我看来，有两种可能：

(Either a Void, Either Void b) -- here I renamed "not b" to "b"
(Either Void b, Either a Void) -- here I renamed "not a" to "a"

但是在这最后一段，我感觉自己只是搞错了事情的来龙去脉。

（相关问题的跟进请参见此处。）

- Enlico

---

Xor的另一个可能的解释是“不同构”。 - luqui

@luqui 为什么？Int和[Int]不是同构的（它们是吗？），但它们都有值，因此都为真，因此它们异或为假。如果这不是情况，那我的错误在哪里？ - Enlico

嗯，是我的错误。我想我是指“不等价”，将等价理解为逻辑意义上的(A -> B) and (B -> A)。这仍然在布尔逻辑中合法地符合异或运算，但它在直觉上比丹尼尔答案中的那个弱。 - luqui

Answer 1

否定的标准技巧是使用-> Void，因此：

type Not a = a -> Void

当且仅当a本身是一个可以被证明为不可居住的类型时，我们才能构建这种类型的完整居民；如果存在a的任何居民，则不能构建此类型的完整居民。听起来像是否定命题！

内联表示，这意味着您的异或定义类似于以下之一：

type Xor a b = (Either a b, (a, b) -> Void) -- (a ∨ b) ∧ ¬(a ∧ b)
type Xor a b = (Either a b, Either (a -> Void) (b -> Void)) -- (a ∨ b) ∧ (¬a ∨ ¬b)

- Daniel Wagner

---

你的第二个版本看起来有些别扭，因为这两个“Either”必须相反。第三种表述方式是：Either (a, b -> Void) (b, a -> Void)。 - dfeuer

@dfeuer，您能详细说明吗？我不明白您是在强调一个不准确之处还是只是事实，即在4个可能的选择中，丹尼尔选择的比其余的更漂亮/难看。 - Enlico

@Enrico，这句话并没有错误。但是使用它来得到其他表达方式需要额外的情况分支来展示荒谬性。 - dfeuer