Next | Types Are Theorems; Programs Are Proofs | 19 |

-- x :: a -- y :: b (x, y) :: (a, b)

In logic if you can prove

*a*and you can prove*b*,Then you may conclude

*a*∧*b*(This is called ∧I)

The analogous programming operation is

*constructing*a pair value