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)
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?
It seems that how to write xor actually boils down to how to write not.
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.)
The standard trick for negation is to use -> Void, so:
type Not a = a -> Void
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!
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)