什么类型对应于类型理论中的 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"

但在最后一段中，我有一种感觉，我只是把狗弄错了。

（在这里跟进问题。）

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)