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

The missing logical operator, ¬ (“not”), is a little funny

It is closely related to ⊥ (“nonsense”):

¬*p* ≡ *p* → ⊥

In Haskell, ⊥ is a type with no elements

It's the type of value that is(n't) returned by an infinite loop

or by a calculation that throws a fatal exception

In practice, it never comes up

The Haskell type checker always infers a more general type:

undefined :: a

loop x = loop x -- loop :: b -> a -- loop x :: a

In Haskell, ¬

*p*≡*p*→ ⊥ is a function that takes*p*and fails to returnIn logic, we have:

From

*p*∧ ¬*p*, conclude ⊥ (`⊥I`)From ⊥, conclude

**anything**(`⊥E`)Easy exercise:

(¬*p* ∧ *p*) → ⊥

`(p -> Void, p) → Void
`

Next | Next |