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.