12

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

Enlico
  • 23,259
  • 6
  • 48
  • 102
  • Another possible interpretation of xor is "not isomorphic" – luqui Oct 16 '20 at 06:20
  • @luqui 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? – Enlico Oct 16 '20 at 06:33
  • 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. – luqui Oct 17 '20 at 02:51

1 Answers1

11

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)
Daniel Wagner
  • 145,880
  • 9
  • 220
  • 380
  • 6
    Your second version seems a bit awkward to me, since the two `Either`s must go opposite ways. A third formulation: `Either (a, b -> Void) (b, a -> Void)`. – dfeuer Oct 16 '20 at 04:14
  • @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. – Enlico Oct 16 '20 at 16:43
  • 1
    @Enrico, nothing inaccurate about it. But using it to get other formulations involves extra case branches to show absurdity. – dfeuer Oct 16 '20 at 17:31