4
$\begingroup$

In Wikipedia article on "Sum Type" it is stated that sum type Curry-Howard correspondence is intuitionistic logical disjoint.

But sum type definition states that it is

a data structure used to hold a value that could take on several different, but fixed, types. Only one of the types can be in use at any one time, and a tag field explicitly indicates which one is in use.

whereas in disjunction you can have both values present at the same time.

To me it looks like sum type is more like a multiplexer than a simple "or", that is $(A\land S) \lor(A \land \lnot S)$, specially because its eliminator acts like a case statement.

I would appreciate if someone can make it clear for me.

$\endgroup$
3
  • 1
    $\begingroup$ In a disjunction $A \lor B$, both $A$ and $B$ can be true, but to witness a proof of $A \lor B$ you use either $A$ or $B$, but not both. In a sum type $A + B$, you can have terms of both type $A$ and type $B$, but to give a term of type $A + B$, you use either the term of type $A$ or the term of type $B$, but not both. $\endgroup$
    – varkor
    Dec 8, 2021 at 17:43
  • 1
    $\begingroup$ @varkor “to witness a proof of A∨B you use either A or B” in intuitionistic logic, yes. But in classical logic, you can use the law of excluded middle and use neither. So in a classical logic proof, you don't have to say that you're using one side of the disjunction or the other. $\endgroup$ Dec 8, 2021 at 18:57
  • $\begingroup$ @Gilles'SO-stopbeingevil': yes, that is a good point, and a good answer. $\endgroup$
    – varkor
    Dec 8, 2021 at 20:17

1 Answer 1

6
$\begingroup$

in disjunction you can have both values present at the same time

In classical logic, yes. But the Curry-Howard correspondence relates basic type theory to intuitionistic logic. And in intuitionistic logic, to speak intuitively, when you know that $A \vee B$ is true, you know which one is true.

The idea of intuitionistic logic is that if you can prove a proposition $P$, it doesn't mean “$P$ is true” (as it does in classical logic), but “I know how to prove $P$”. When the proposition is of the form $A \vee B$, the way to prove $A \vee B$ must either involve a proof of $A$ or a proof of $B$, plus the information of which side you chose to prove. This is not true in classical logic, which has $A \vee \neg A$ as an axiom, which doesn't tell you which of $A$ or $\neg A$ is true or how you'd prove it. The absence of this axiom, the excluded middle, is the defining feature of intuitionistic logic compared to classical logic.

It's possible to extend the Curry-Howard correspondence to classical logic, but this require a more complex type system, and the classical disjunction won't map to a sum type.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.