| Next | Types Are Theorems; Programs Are Proofs | 24 |
On the programming side, a ∨ b is a union type
It could contain a value of type a or a value of type b
(Plus a tag telling you which one it is)
In Haskell this is written Either a b
There are two injectors for constructing union values:
-- x :: a
-- y :: b
Left x :: Either a b
Right y :: Either a b
| Next | Next |