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

Very cool to see the constructive code for the proof of double negation in intuitionistic logic. But what about the Curry-Howard correspondence for classical logic? What would the classical code for the classical proof of excluded middle look like? On Fri, May 15, 2020 at 11:09 PM 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 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-progr...

-- -- 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.

_______________________________________________ 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.

-- -- Kim-Ee