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

[Olaf Klinke]

Indeed, Chris, I also could not come up with a proof without use of
deMorgan's law. When you remove the type annotations in your code, you
obtain an inhabitant of the following type. 

forall a r. ((Either a (a -> r)) -> r) -> r

-- Lemma: reverse of 'either', your deMorgan generalized. 
un_either :: (Either a b -> c) -> (a -> c,b -> c)
un_either f = (f . Left,f . Right)
uncurry (flip ($)) . un_either 
  :: (Either a (a -> r) -> r) -> r

There is a geometric interpretation of intuitionistic double negation. 
Consider an open set A on the real line, an interval without end
points, say. As it is custom, I will "draw" open intervals with round
parentheses.

        A
-----(======)----- 

Open sets form a Heyting algebra, where (&&) is implemented by set
intersection, (||) is implemented by set union and which has an
implication (->), but only the laws of intuitionistic logic hold. This
correspondence helps me a lot when thinking about terms of the logic.
The Heyting negation of an open set on the real line is the interior of
the set complement:

-----(======)----- A
=====]------[===== set complement of A
=====)------(===== Not A

Here "interior" means the set with all boundary points removed. 
Now what is a set where Not (Not A) is True? It is "dense", a set that
is so fat that when you do the Heyting negation twice, it covers the
entire real line. One class of such sets are the real line without a
single point: 

=====)(===== A
------------ Not A 
============ Not (Not A)

This is because the interior of a single point (the set complement of
A) is the empty set, and the complement of the empty set is the entire
real line. 
In that respect you could say that the law of excluded middle is almost
true in intuitionistic logic. 

Heyting negation is a special case of Heyting implication. The Heyting
implication A -> B of two open sets A and B is the largest open set C
whose intersection with A is contained in B. (Equivalently, the largest
C that has the same intersection with A as B has. These definitions
also hold for classical implication and the Boolean algebra of all
sets.)

-----(======)----- A
---------(=====)-- B
---------(==)----- A && B
=====)---(======== A -> B

Exercise: Convince yourself, using the definition of A -> B given
above, that A -> B is the entire real line if and only if A is
contained in B.
Now consider the types of 'curry' and 'uncurry' and squint a little:

'curry' and 'uncurry' are witnesses for the isomorphism of types

((c,a) -> b) ~ (c -> (a -> b)).

Read this as:

( c     ,         a)     ->         b
(c `intersection` a) `contained in` b

if and only if

c      ->        (a       ->      b)
c `contained in` (a `implication` b)

Olaf

On Fri, 2020-05-15 at 12:04 -0400, Chris Smith wrote:
> This was indeed a fun puzzle to play with.  I think this becomes
> easier to
> interpret if you factor out De Morgan's Law from the form you posted
> at the
> beginning of your email.
> 
> https://code.world/haskell#PYGDwpaMZ_2iSs74NnwCUrg
> 
> 
> On Fri, May 15, 2020 at 5:23 AM Ruben Astudillo <
> ruben.astud at gmail.com>
> wrote:
> 
> > On 13-05-20 09:15, Olaf Klinke wrote:
> > > Excersise: Prove that intuitionistically, it is absurd to deny
> > > the law
> > > of excluded middle:
> > > 
> > > Not (Not (Either a (Not a)))
> > 
> > It took me a while but it was good effort. I will try to explain
> > how I
> > derived it. We need a term for
> > 
> >    proof :: Not (Not (Either a (Not a)))
> >    proof :: (Either a (Not a) -> Void) -> Void
> > 
> > A first approximation is
> > 
> >    -- Use the (cont :: Either a (Not a) -> Void) to construct the
> > Void
> >    -- We need to pass it an Either a (Not a)
> >    proof :: (Either a (Not a) -> Void) -> Void
> >    proof cont = cont $ Left <no a to fill in>
> > 
> > Damn, we can't use the `Left` constructor as we are missing an `a`
> > value
> > to fill with. Let's try with `Right`
> > 
> >    proof :: (Either a (Not a) -> Void) -> Void
> >    proof cont = cont $ Right (\a -> cont (Left a))
> > 
> > Mind bending. But it does make sense, on the `Right` constructor we
> > assume we are have an `a` but we have to return a `Void`. Luckily
> > we can
> > construct a `Void` retaking the path we were gonna follow before
> > filling
> > with a `Left a`.
> > 
> > Along the way I had other questions related to the original mail
> > and
> > given you seem knowledgeable I want to corroborate with you. I've
> > seen
> > claimed on the web that the CPS transform *is* the double negation
> > [1]
> > [2]. I don't think that true, it is almost true in my view. I'll
> > explain, these are the types at hand:
> > 
> >     type DoubleNeg a = (a -> Void) -> Void
> >     type CPS a = forall r. (a -> r) -> r
> > 
> > We want to see there is an equivalence/isomorphism between the two
> > types. One implication is trivial
> > 
> >     proof_CPS_DoubleNeg :: forall a. CPS a -> DoubleNeg a
> >     proof_CPS_DoubleNeg cont = cont
> > 
> > We only specialized `r ~ Void`, which mean we can transform a `CPS
> > a`
> > into a `DoubleNeg a`. So far so good, we are missing the other
> > implication
> > 
> >     -- bind type variables: a, r
> >     -- cont   :: (a -> Void) -> Void
> >     -- absurd :: forall b. Void -> b
> >     -- cc     :: a -> r
> >     proof_DoubleNeg_CPS :: forall a. DoubleNeg a -> CPS a
> >     proof_DoubleNeg_CPS cont = \cc -> absurd $ cont (_missing . cc)
> > 
> > Trouble, we can't fill `_missing :: r -> Void` as such function
> > only
> > exists when `r ~ Void` as it must be the empty function. This is
> > why I
> > don't think `CPS a` is the double negation.
> > 
> > But I can see how people can get confused. Given a value `x :: a`
> > we can
> > embed it onto `CPS a` via `return x`. As we saw before we can pass
> > from
> > `CPS a` to `DoubleNeg a`. So we have *two* ways for passing from
> > `a` to
> > `DoubleNeg a`, the first one is directly as in the previous mail.
> > The
> > second one is using `proof_CPS_DoubleNeg`
> > 
> >     embed_onto_DoubleNeg :: a -> DoubleNeg
> >     embed_onto_DoubleNeg = proof_CPS_DoubleNeg . return
> >       where
> >         return :: a -> CPS a
> >         return a = ($ a)
> > 
> > So CPS is /almost/ the double negation. It is still interesting
> > because
> > it's enough to embed a classical fragment of logic onto the
> > constructive
> > fragment (LEM, pierce etc). But calling it a double negation really
> > tripped me off.
> > 
> > Am I correct? Or is there other reason why CPS is called the double
> > negation transformation?
> > 
> > Thank for your time reading this, I know it was long.
> > 
> > [1]: http://jelv.is/talks/curry-howard.html#slide30
> > [2]:
> > 
> > https://www.quora.com/What-is-continuation-passing-style-in-functional-programming
> > 
> > --
> > -- Rubén
> > -- pgp: 4EE9 28F7 932E F4AD
> > 
> > _______________________________________________
> > 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.