类型理论中与xor b对应的类型是什么? [英] What type corresponds to a xor b in type theory?
问题描述
在类别理论8.2 的末尾，巴托斯·米列夫斯基(Bartosz Milewski)显示了一些示例逻辑，范畴论和类型系统之间的对应关系.
At the end of Category Theory 8.2, Bartosz Milewski shows some examples of the correspondence between logic, category theory, and type systems.
我在徘徊与逻辑异或运算符相对应的内容.我知道
I was wandering what corresponds to the logical xor operator. I know that
a xor b == (a ∨ b) ∧ ¬(a ∧ b) == (a ∨ b) ∧ (¬a ∨ ¬b)
所以我只解决了部分问题:a xor b对应于(Either a b, Either ? ?).但是，缺少的两种类型是什么?
so I've solved only part of the problem: a xor b corresponds to (Either a b, Either ? ?). But what are the two missing types?
xor的写法实际上归结为not的写法.
It seems that how to write xor actually boils down to how to write not.
那么¬a是什么?我的理解是，如果存在类型为a的元素(至少一个)，则a是逻辑上正确的.因此，要使not a为true，a应该为false，即它应该为Void.因此，在我看来，有两种可能性:
So what is ¬a? My understanding is that a is logical true if there exist an element (at least one) of type a. So for not a to be true, a should be false, i.e. it should be Void. Therefore, it seems to me that there are two possibilities:
(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"
但是在最后一段中，我有种感觉，就是我弄错了那只狗.
But in this last paragraph I have the feeling I'm just getting the wrong end of the dog.
(Follow up question here.)
推荐答案
否定的标准技巧是使用-> Void，因此:
The standard trick for negation is to use -> Void, so:
type Not a = a -> Void
当a本身是可证明的无人居住类型时，我们可以精确地构造此类型的全部居民.如果有a的任何居民，我们将无法构造此类型的全部居民.听起来像是对我的否定！
We can construct a total inhabitant of this type exactly when a is itself a provably uninhabited type; if there are any inhabitants of a, we cannot construct a total inhabitant of this type. Sounds like a negation to me!
内联，这意味着您对xor的定义看起来像其中之一:
Inlined, this means your definition of xor looks like one of these:
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)
这篇关于类型理论中与xor b对应的类型是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
