[Haskell-cafe] Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

[Olaf Klinke]

> 2. Double negation enables a translation of classical logic in 
> intuitionistic logic, here embedded in Haskell:
> 
Below I'll give a variant of Li-yao's logic language in Haskell98. 
Again, the open set model may help to visualize CPS translation: 

Consider all open sets A on the real line which are fixed points of
double negation. All intervals are of this kind, but poking holes in
them destroys this property:

---(====)(====)--- A
===)----------(=== Not A
---(==========)--- Not (Not A)

Denote the collection of open sets invariant under double negation by
X. As the example above demonstrates, X is not closed under set union.
But set intersection preserves membership of X. So we have a funny
logic that has (&&) but no (||). The CPS trick is now to define a new
(||) by means of double negation:

---(====)--------- A
---------(====)--- B
---(====)(====)--- set union of A and B
---(==========)--- A || B, double negation of set union.

In fact X is the largest Boolean algebra contained in the Heyting
algebra of open sets. In terms of Haskell, we define a new Either:

Either' a b = ((Either a b) -> Void) -> Void

Looks familiar? Indeed, in this thread we already proved

Either' a (Not a).

This says that Not A is the Boolean complement of A in X. Using (,) and
Either' for (&&) and (||) you can realize all proofs of classical
propositional logic in Haskell without GADTs. 

Olaf