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

Sat May 16 19:56:51 UTC 2020

```> 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