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

Jinxuan Zhu zhujinxuan at gmail.com
Sun May 17 07:47:06 UTC 2020

```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
>
>
> 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
>
> Olaf
>
> _______________________________________________
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...