Next Types Are Theorems; Programs Are Proofs 25

Union types

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

Next Next