What type corresponds to a xor b in type theory?

Question

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.)

Thecla

Another possible interpretation of xor is "not isomorphic" – Vasoinhibitor

@Vasoinhibitor why? Int and [Int] are not isomorphic (are they?), but they are both inhabitated, hence both true, hence they xor to false. I'd this is not the case, where's my mistake? – Thecla

hmm, yes my mistake. I guess I meant "not equivalent", taking equivalent in the logical sense (A -> B) and (B -> A). This still lawfully conforms to xor from boolean logic, but it is intuitionistically weaker than the one in Daniel's answer. – Vasoinhibitor

Answer 1

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)

Meldameldoh

Your second version seems a bit awkward to me, since the two Eithers must go opposite ways. A third formulation: Either (a, b -> Void) (b, a -> Void). – Arneson

@dfeuer, can you elaborate? I don't understand if you are highlighting an inaccuracy or just the fact that, among the 4 possible choices, those chosen by Daniel are nicer/uglier than the remaining ones. – Thecla

@Enrico, nothing inaccurate about it. But using it to get other formulations involves extra case branches to show absurdity. – Arneson