Actually I called it that because it's derived from the law of excluded middle: "A OR not A" is always true.

You can encode logical statements in the Haskell type system as follows:

  a OR b: Either a b

  a AND b: ( a, b )

  not A: a -> Void

  a implies b: a -> b

With this encoding, having a well-formed value for a given type is a proof of its validity.

The one thing we can't use directly is double negation, because we would have to make A appear out of nowhere:

  ((a -> Void) -> Void) -> a

However, this is exactly the type of Cont Void. This means we can use the Cont Void monad to make logical proofs, including double negation. The type:

  Cont Void (Either (a -> Void) a))

Encodes the law of excluded middle, and the value I wrote is a proof of it. It so happens that you can use a type parameter instead of Void because an arbitrary type can also not be used for anything.