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 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."
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)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With