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

-- z :: (a, b) fst z :: a snd z :: b

In logic if you can prove

*a*∧*b*,then you may conclude

*a*you may also conclude

*b*(These are called ∧E)

The analogous programming operation is

*destructing*a pair value

Next | Next |