Just want to post some other things if someone is interested about using Yoneda. Because Void -> a is unique, (Yo void) is terminal in [C, Set]. We can convert the (a -> void) -> (b -> void) as Yo a ~> Yo b. Some details are attached. On Sat, May 16, 2020, 3:58 PM Olaf Klinke wrote:

...

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

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.