If Either can be either Left or Right but not both, then why does it correspond to OR instead of XOR in Curry-Howard correspondence?

Question

When I asked this question, one of the answers, now deleted, was suggesting that the type Either corresponds to XOR, rather than OR, in the Curry-Howard correspondence, because it cannot be Left and Right at the same time.

Where is the truth?

Supervise

Answer 1

The confusion stems from the Boolean truth-table exposition of logic. In particular, when both arguments are True, OR is True, whereas XOR is False. Logically it means that to prove OR it's enough to provide the proof of one of the arguments; but it's okay if the other one is True as well--we just don't care.

In Curry-Howard interpretation, if somebody gives you an element of Either a b, and you were able to extract the value of a from it, you still know nothing about b. It could be inhabited or not.

On the other hand, to prove XOR, you not only need the proof of one argument, you must also provide the proof of the falsehood of the other argument.

So, with Curry-Howard interpretation, if somebody gives you an element of Xor a b and you were able to extract the value of a from it, you would conclude that b is uninhabited (that is, isomorphic to Void). Conversely, if you were able to extract the value of b, then you'd know that a was uninhabited.

The proof of falsehood of a is a function a->Void. Such a function would be able to produce a value of Void, given a value of a, which is clearly impossible. So there can be no values of a. (There is only one function that returns Void, and that's the identity on Void.)

Trilemma

for me, the key in your answer is its last sentence. thanks for saying it, others didn't. no one bothered to state the obvious, but it is the obvious that isn't known at all to a new learner. I kept trying to find such a function (besides undefined), but the point was exactly that it didn't exist. that means e.g. XOR Char Int value doesn't exist either. now it's clear what all this stuff is about. always state the obvious! thanks again. ---- so, saying a -> Void exists is the same as saying a ~ Void. (there probably is no other way to say it in ("simple"?) Haskell). correct? – Arneson

@WillNess, not ~ in the Haskell sense. Void is unique up to unique isomorphism. f :: XOR Char Int -> Void exists, and is unique. absurd is its unique inverse. – Bow

@Bow according to Bartosz's answer, f = id. so that must mean XOR Char Int unifies with Void? – Arneson

@WillNess, I think he was being a bit loose in his writing. – Bow

do you mean e.g. with your type, type XOR a b = Either (a, b -> Void) (b, a -> Void), something like f :: XOR Char Int -> Void ; f (Left (char,int_void)) = int_void 1; f (Right (int,char_void)) = char_void 'a'? and then the point of it is, that int_void and char_void are non-existent? – Arneson

@WillNess, yes. There are lots of empty types, all of them equivalent (isomorphic) in the most boring possible way (there's exactly one isomorphism between each pair). This is a general property of initial objects in category theory. Let V1 and V2 be initial objects. By def of init obj, there are unique f :: V1 -> V2, g :: V2 -> V1. f . g :: V2 -> V2 and g . f :: V1 -> V1. By uniqueness, f . g = id_V2 and g . f = id_V1. Why are empty types initial objects in Hask? There can be no meaningful difference between two functions when neither can actually be called. – Bow

@Bow thank you, this whole thing does become a bit clearer now. – Arneson

Answer 2

If you have a value of type P and a value of type Q (that is, you have both a proof of P and a proof of Q), then you are still able to provide a value of type Either P Q.

Consider

x :: P
y :: Q
...

z :: Either P Q
z = Left x    -- Another possible proof would be `Right y`

While Either does not have a specific case that explicitly represents this situation (unlike These), it does not do anything to exclude it (as in exclusive OR).

This third case where both have proofs is a bit different than the other two cases where only one has a proof, which reflects the fact that "not excluding" something is a bit different than "including" something in intuitionistic logic, since Either does not provide a particular witness for this fact. However Either is not an XOR in the way that XOR would typically work since, as I said, it does not exclude the case where both parts have proofs. What Daniel Wagner proposes in this answer, on the other hand, is much closer to an XOR.

Either is kind of like an exclusive OR in terms of what its possible witnesses are. On the other hand, it is like an inclusive OR when you consider whether or not you can actually create a witness in four possible scenarios: having a proof of P and a refutation of Q, having a proof of Q and a refutation of P, having a proof of both or having a refutation of both.^[1] While you can construct a value of type Either P Q when you have a proof of both P and Q (similar to an inclusive OR), you cannot distinguish this situation from the situation where only P has a proof or only Q has a proof using only a value of type Either P Q (kind of similar to an exclusive OR). Daniel Wagner's solution, on the other hand, is similar to exclusive OR on both construction and deconstruction.

It is also worth mentioning that These more explicitly represents the possibility of both having proofs. These is similar to inclusive OR on both construction and deconstruction. However, it's also worth noting that there is nothing preventing you from using an "incorrect" constructor when you have a proof of both P and Q. You could extend These to be even more representative of an inclusive OR in this regard with a bit of additional complexity:

data IOR a b
  = OnlyFirst  a       (Not b)
  | OnlySecond (Not a) b
  | Both       a       b

type Not a = a -> Void

The potential "wrong constructor" issue of These (and the lack of a "both" witness in Either) doesn't really matter if you are only interested in a proof irrelevant logical system (meaning that there is no way to distinguish between any two proofs of the same proposition), but it might matter in cases where you want more computational relevance in the logic.^[2]

In the practical situation of writing computer programs that are actually meant to be executed, computational relevance is often extremely important. Even though 0 and 23 are both proofs that the Int type is inhabited, we certainly like to distinguish between the two values in programs, in general!

Regarding "construction" and "destruction"

Essentially, I just mean "creating values of a type" by construction and "pattern matching" by destruction (sometimes people use the words "introduction" and "elimination" here, particularly in the context of logic).

In the case of Daniel Wagner's solutions:

• Construction: When you construct a value of type Xor A B, you must provide a proof of exactly one of A or B and a refutation of the other one. This is similar to exclusive or. It is not possible to construct a value of this unless you have a refutation of either A or B and a proof of the other one. A particularly significant fact is that you cannot construct a value of this type if you have a proof of both A and B and you don't have a refutation of either of them (unlike inclusive OR).

• Destruction: When you pattern match on a value of type Xor A B, you always have a proof of one of the types and a refutation of the other. It will never give you a proof of both of them. This follows from its definition.

In the case of IOR:

• Construction: When you create a value of type IOR A B, you must do exactly one of the following: (1) provide only a proof of A and a refutation of B, (2) provide a proof of B and a refutation of B, (3) provide a proof of both A and B. This is like inclusive OR. These three possibilities correspond exactly to each of the three constructors of IOR, with no overlap. Note that, unlike the situation with These, you cannot use the "incorrect constructor" in the case where you have a proof of both A and B: the only way to make a value of type IOR A B in this case is to use Both (since you would otherwise need to provide a refutation of either A or B).

• Destruction: Since the three possible situations where you have a proof of at least one of A and B are exactly represented by IOR, with a separate constructor for each (and no overlap between the constructors), you will always know exactly which of A and B are true and which is false (if applicable) by pattern matching on it.

Pattern matching on IOR

Pattern matching on IOR works exactly like pattern matching on any other algebraic datatype. Here is an example:

x :: IOR Char Int
x = Both 'c' 3

y :: IOR Char Void
y = OnlyFirst 'a' (\v -> v)

f :: Not p -> IOR p Int
f np = OnlySecond np 7

z :: IOR Void Int
z = f notVoid

g :: IOR p Int -> Int
g w =
  case w of
    OnlyFirst  p q -> -1
    OnlySecond p q -> q
    Both       p q -> q

-- We can show that the proposition represented by "Void" is indeed false:
notVoid :: Not Void
notVoid = \v -> v

Then a sample GHCi session, with the above code loaded:

ghci> g x
3
ghci> g z
7

---

^[1]This gets a bit more complex when you consider that some statements are undecidable and therefore you cannot construct a proof or a refutation for them.

^[2]Homotopy type theory would be one example of a proof relevant system, but this is reaching the limit of my knowledge as of now.

Pals

David, I think I understand most of your answer; however I'm still puzzled by the bit where you write Daniel Wagner's solution, on the other hand, is similar to exclusive OR on both construction and deconstruction; later you mention inclusive OR on both construction and deconstruction as well. Could you clarify that parts a bit? I guess that examples like "I can declare this value but not this" (as you did in the first chunk of code) would help me understand your point, maybe. – Supervise

Another thing that would probably help me is how I would use IOR. For instance, I see I can pattern-match against Both, as in Both a b = Both 3 'c' :: IOR Int Char is just fine and does what I expected. But how would I use OnlyFirst? Can I pattern match against it? This seems to be somewhat related to your mention of constrution and deconstruction, no? – Supervise

@Enrico I added a bit more to the answer about that. Does that help? – Pals

It certainly helps. However I want to take some time to look carefully at the three answers together, as there's still something quite not clear to me. – Supervise

Answer 3

Perhaps try replacing “proof” in the Curry-Howard isomorphism with “evidence”.

Below I will use italics for propositions and proofs (which I will also call evidence), the mathematical side of the isomorphism, and I will use code for types and values.

The question is: suppose I know the type for [values corresponding to] evidence that P is true (I will call this type P), and I know the type for evidence that Q is true (I call this type Q), then what is the type for evidence of the proposition R = P OR Q?

Well there are two ways to prove R: we can prove P, or we can prove Q. We could prove both but that would be more work than necessary.

Now ask what the type should be? It is the type for things which are either evidence of P or evidence of Q. I.e. values which are either things of type P or things of type Q. The type Either P Q contains precisely those values.

What if you have evidence of P AND Q? Well this is just a value of type (P, Q), and we can write a simple function:

f :: (p,q) -> Either p q
f (a,b) = Left a

And this gives us a way to prove P OR Q if we can prove P AND Q. Therefore Either cannot correspond to xor.

---

What is the type for P XOR Q?

At this point I will say that negations are a bit annoying in this sort of constructive logic.

Let’s convert the question to things we understand, and a simpler thing we don’t:

P XOR Q = (P AND (NOT Q)) OR (Q AND (NOT P))

Ask now: what is the type for evidence of NOT P?

I don’t have an intuitive explanation for why this is the simplest type but if NOT P were true then evidence of P being true would be a contradiction, which we say as proving FALSE, the unprovable thing (aka BOTTOM or BOT). That is, NOT P may be written in simpler terms as: P IMPLIES FALSE. The type for FALSE is called Void (in haskell). It is a type which no values inhabit because there are no proofs of it. Therefore if you could construct a value of that type you would have problems. IMPLIES corresponds to functions and so the type corresponding to NOT P is P -> Void.

We put this with what we know and get the following equivalence in the language of propositions:

P XOR Q = (P AND (NOT Q)) OR (Q AND (NOT P)) = (P AND (Q IMPLIES FALSE)) OR ((P IMPLIES FALSE) AND Q)

The type is then:

type Xor p q = Either (p, q -> Void) (p -> Void, q)

Millstream

I follow you up to a point, but you got me at I don't have an..., :/ – Supervise

Yeah, I think it’s just unintuitive when you introduce FALSE (ie BOT) into logic. Maybe think of it as CONTRADICTION instead. If you can prove some contradiction, you can prove anything (because FALSE IMPLIES P for any P). Therefore proving NOT P means providing that if it were true you would have a contradiction. – Millstream

It's worth mentioning that property of contradictions you mention is known as the principle of explosion, sometimes referred to as "ex falso quodlibet". Also, as an aside, Void is isomorphic to forall a. a (not really making a particular point, just thought that could be generally useful to mention). – Pals