14

在范畴论 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如果存在 type 的元素（至少一个），这是合乎逻辑的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"

但在最后一段中，我觉得我只是弄错了狗的结局。

（在此处跟进问题。）

4

1 回答 1

12

否定的标准技巧是使用-> 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)
于 2020-10-15T21:51:35.847 回答