Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What type corresponds to a xor b in type theory?

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

like image 650
Enlico Avatar asked Oct 15 '20 21:10

Enlico


People also ask

What is a logical XOR?

The XOR ( exclusive-OR ) gate acts in the same way as the logical "either/or." The output is "true" if either, but not both, of the inputs are "true." The output is "false" if both inputs are "false" or if both inputs are "true."


Video Answer


1 Answers

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)
like image 86
Daniel Wagner Avatar answered Oct 17 '22 17:10

Daniel Wagner