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