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 making union values:
-- x :: a -- y :: b Left x :: Either a b Right y :: Either a b
continued...
Next | Copyright © 2014 M. J. Dominus |