Union types

• How do you use a value of type Either a b?

• It's a little complicated

• In Haskell it looks like this:

        -- z :: Either a b

        case z of
          Left  x ->
             … x …            --   a -> c
          Right y ->
             … y …            --   b -> c

            :: c

• In logic if you know a ∨ b

• and can prove a → c

• and can prove b → c

• then you may conclude c

• (This is ∨E)