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

older
Re: [Haskell-cafe] Relationship...

Olaf Klinke

13 May 2020 13 May '20

1:15 p.m.

You're misplacing your quantifiers.

(a -> Void) -> Void)

is not isomorphic to

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

but *is* isomorphic to

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

...which is because you could _define_ Void to be (forall r. r): {-# LANGUAGE Rank2Types #-} newtype Void = Void {absurd :: forall r. r} In practice, Void used to be implemented as data Void = Void Void before it became just data Void by means of EmptyDataDecls extension. The latter has the advantage that there is no constructor named 'Void'. In reality of course, Void does have an element, bottom, which it shares with all other types. Hence the 'absurd' function that returns the bottom in type r when given the bottom in type Void. But as you know the correspondence between types and theorems in intuitionistic logic explicitly regards only total values. Excersise: Prove that intuitionistically, it is absurd to deny the law of excluded middle: Not (Not (Either a (Not a))) There is a whole world to be discovered beneath the total values. Think about the type () as truth values and what universal quantification could be. Olaf

Show replies by date

Ruben Astudillo

15 May 15 May

9:19 a.m.

New subject: Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

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

Chris Smith

4:04 p.m.

New subject: Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

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.

Olaf Klinke

7:20 p.m.

New subject: Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

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

Olaf Klinke

16 May 16 May

8:41 a.m.

New subject: Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

As usual, Edward Kmett has the answer for anything categorical in Haskell. The type CPS a = forall r. (a -> r) -> r is isomorphic to Yoneda Identity a = forall r. (a -> r) -> Identity r and the latter is the Yoneda embedding [1] of the Identity functor. The Yoneda Lemma [2,3] states that for any functor f, the Yoneda embedding of f is isomorphic to f. We conclude that CPS a is isomorphic to a, and the relationship you found with Void is akin to the fact that in any Heyting algebra, any element is smaller than its double negation. Olaf [1] https://hackage.haskell.org/package/kan-extensions/docs/Data-Functor-Yoneda.... See also the blog post linked at the top of that page. [*] [2] https://en.wikipedia.org/wiki/Yoneda_lemma [3] https://ncatlab.org/nlab/show/Yoneda+embedding [*] Fun fact: If you install a Haskell package and watch which dependencies are build, surprisingly often kan-extensions is among them. You'd think: What the hell does category theory have to do with my program? But hey, this is a Haskell program you're writing, so you really should not be surprised.

Kim-Ee Yeoh

18 May 18 May

1 a.m.

New subject: 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

David Feuer

1:19 a.m.

New subject: Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

Classically, the excluded middle is an axiom, not a theorem. There is no code/proof. On Sun, May 17, 2020, 9:02 PM Kim-Ee Yeoh wrote:

...

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

7:52 a.m.

New subject: Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

On Mon, May 18, 2020 at 8:19 AM David Feuer wrote:

...

Classically, the excluded middle is an axiom, not a theorem.

Untrue in general.

...

On Sun, May 17, 2020, 9:02 PM Kim-Ee Yeoh wrote:

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

Ruben Astudillo

3:05 a.m.

New subject: Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

On 17-05-20 21:00, Kim-Ee Yeoh wrote:

...

But what about the Curry-Howard correspondence for classical logic?

Curry-Howard only offers a translation between a fragment of logic that is constructive logic and the typed lambda calculus. But that is not the whole story, we can embed classical logic into constructive logic via the the "double negation translation" [1]. How is such thing possible? The idea is that classical logic is constructive logic with an extra axiom. That extra axiom can either be Pierce's Law, the excluded middle or the double negation elimination. Which ever you "add" to your constructive logic will make it a classical logic. Here is the trick, to whatever proposition `a` that we want to prove, we can "add" an extra postulate for a non-local jump as an argument and call that proposition `CPS a`. That way, when proving/constructing the term inside the CPS-code, you will have at your hand an extra argument that will allow you to fill the extra power needed by classical proofs [1]. It's interesting to note that operationally, what classical proofs can do that constructive proofs cannot is the ability to do non-local jumps, there represented by the continuation. Harper's course given at [2] has been my fun the last few days and explains it in greater detail.

...

What would the classical code for the classical proof of excluded middle look like?

As in the previous mails type Not a = a -> Void type CPS a = (a -> Void) -> Void proof :: CPS (Either a (Not a)) proof = \cont -> cont $ Right (\a -> cont (Left a)) Modulo my point between the different representations of CPS and their relation to the double negation, that code only type check because terms under CPS have access to an extra non-local jump to allow classical arguments. Even so this code is *good* as shows explicitly when the non-local jumps happen and the rest of the code is constructive. [1]: https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts/class.pdf [2]: https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts -- -- Rubén -- pgp: 4EE9 28F7 932E F4AD

Li-yao Xia

15 May 15 May

9:59 p.m.

New subject: Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

Hi Ruben,

...

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

You're reading too much into this claim. When I read "CPS", I would think of types of the form ((a -> r) -> r), but how the r gets instantiated or quantified is very context-dependent. Note that (forall r. (a -> r) -> r) is isomorphic to a. From that, you can conclude that it is not isomorphic to ((a -> Void) -> Void). Looking at types only, the correspondence between double negation and CPS is only a superficial observation that ((a -> Void) -> Void) matches ((a -> r) -> r) simply by setting (r = Void). But CPS is a program transformation before all. Therefore, to understand the correspondence with double negation, we should really be looking at the level of terms (programs or proofs). 1. Define a language of proofs in classical logic. Below is one of many ways of doing it, notably featuring a rule for double-negation elimination (NotNot). A term (x :: K a) is a proof of the proposition a. data K a where AndI :: K a -> K b -> K (a :*: b) OrIL :: K a -> K (a :+: b) OrIR :: K b -> K (a :+: b) ImplI :: (a -> K b) -> K (a :->: b) Assumption :: a -> K a Cut :: K (a :->: b) -> K a -> K b NotNot :: K (Not (Not a)) -> K a 2. Double negation enables a translation of classical logic in intuitionistic logic, here embedded in Haskell: translate :: K a -> Not (Not a) translate (NotNot p) k = translate p \f -> f k translate (Cut pf px) k = translate pf \f -> translate px \x -> f x k {- etc. -} {- also omitted: the translation of formulas ((:*:), (:+:), (:->:), Not) which is performed implicitly in the above definition of K. -} Full gist: https://gist.github.com/Lysxia/d90afbe716163b03acf765a2e63062cd The point is that the proof language K is literally a programming language (with sums, products, first-order functions, and a weird operator given by double negation elimination), and the "translate" function is literally an interpreter in the programming sense, which one might call a "shallowly embedded compiler", where the target language is in continuation-passing style. Thus, CPS transformation and double-negation translation don't just look similar; when phrased in a certain way, they are literally the same thing. The translation is not unique. There are multiple flavors of "CPS transformation" (or "double-negation translation") depending on where exactly negations are introduced in the translation of formulas. Cheers, Li-yao On 5/15/20 5:19 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...

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

Ingo Blechschmidt

16 May 16 May

12:54 p.m.

New subject: Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

On Fri 15 May 2020 05:19:01 AM GMT, 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)))

This fact is indeed truly wondrous. I encourage everyone to ponder it thoroughly. It has been worked into a classical logic fairy tale: http://blog.ezyang.com/2013/04/a-classical-logic-fairy-tale/ (sorry for http) And more in this little Oleg jewel: https://web.archive.org/web/20180901035449/http://okmij.org/ftp/Computation/...

...

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

Yes, you are right, and your analysis of the situation is correct. Using (_ → R) → R for some fixed statement R instead of ¬¬_ = ((_ → ⊥) → ⊥) is what's called "the R-Friedman translation applied to the double negation translation". It is what powers "Friedman's trick", a marvelous technique for extracting constructive content from classical proofs [1]. People say that you cannot escape the continuation monad. But sometimes, you can. Dickson's lemma nicely illustrates this insight. It states that for any infinite list xs ∷ [Nat], there is an index i such that xs !! i ≤ xs !! (i + 1). This lemma has a trivial classical proof (just pick the minimum of the list xs), but this classical proof is not effective: There is no algorithm for computing the minimum of an infinite list. Using the continuation monad, we can extract the constructive content of this classical proof. See here: https://github.com/iblech/talk-constructive-mathematics/blob/master/law-of-e... Cheers, Ingo [1] Say you want to constructively prove A → B. You already have a classical proof of A → B, and you managed [2] to turn this proof into a constructive proof of ((A → R) → R) → ((B → R) → R), for any as of yet undecided statement R. Now specialize to R ≔ B. Hence we have a constructive proof of ((A → B) → B) → ((B → B) → B). Combining this with the constructive tautologies A → ((A → B) → B) and ((B → B) → B) ↔ B, we obtain a constructive proof of A → B. [2] A metatheorem states that if some statement A is classically provable then its double negation translation and furthermore the R-Friedman translation of the double negation translation are constructively provable. (Incidentally, this metatheorem has a constructive proof.) But "translation" here means more than just replacing A by ¬¬A (respectively ((A → R) → R)). It means introducing a double negation in front of every equality, disjunction and existential quantification. For instance, the ¬¬-translation of ∀x. ∃y. f(x,y) = g(x,y) is ∀x. ¬¬∃y. ¬¬(f(x,y) = g(x,y)). In some circumstances, the double negation translation of a complex statement A is constructively equivalent to ¬¬A, that is, in some circumstances the many nested double negations can be pulled to the front. This is for instance the case for so-called "geometric formulas", statements in which the logical symbols "→" and "∀" don't occur.

1875

Age (days ago)

1880

Last active (days ago)

List overview

Download

10 comments

7 participants

participants (7)

Chris Smith
David Feuer
Ingo Blechschmidt
Kim-Ee Yeoh
Li-yao Xia
Olaf Klinke
Ruben Astudillo

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

tags

participants (7)