[Haskell-cafe] Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)
Olaf Klinke
olf at aatal-apotheke.de
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
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
More information about the Haskell-Cafe
mailing list