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

[Jinxuan Zhu]

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 <olf at aatal-apotheke.de> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200517/efadee91/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: IMG_20200517_033939.jpg
Type: image/jpeg
Size: 4424494 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200517/efadee91/attachment-0001.jpg>