Why is sum-type a disjunction in the Curry-Howard correspondence?

user_15392815 0
Viewed 44

According to the Curry-Howard correspondence the sum-type aka tagged-union is the equivalent of disjunction, logical OR

Why is this the case? Is it not closer to XOR? (a or b) implies that it could be a or b or both, whereas Either a b must be a or b but never both.

curry-howard category-theory
1 Answers

Curry-Howard correspondence says that an element of Either a b represents a proof of a or b. To prove a disjunction it's enough to prove (provide an element of) a or b. You do this by constructing Either a b using either Left a or Right b.

user_900880
Related