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 |