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 t

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.