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 |