haskell - 什么类型对应于类型论中的 xor b？

Question

在 Category Theory 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"

但在最后一段中，我觉得我只是弄错了狗的结局。
(跟进问题 here。)

Answer 1

否定的标准技巧是使用 -> Void ， 所以:

type Not a = a -> Void

我们可以在 a 时构造出这种类型的总居民。本身就是可证明无人居住的类型；如果有 a 的任何居民，我们不能构建这种类型的总居民。听起来像是对我的否定!
内联，这意味着您对 xor 的定义看起来像以下之一:

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)