patternMinor
Is sum type a disjoint or more of a multiplexer?
Viewed 0 times
moretypemultiplexerdisjointsum
Problem
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.
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.
Solution
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.
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.
Context
StackExchange Computer Science Q#146515, answer score: 6
Revisions (0)
No revisions yet.