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

[Kim-Ee Yeoh]

On Mon, May 18, 2020 at 8:19 AM David Feuer <david.feuer at gmail.com> 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 <ky3 at atamo.com> 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 <cdsmith at gmail.com> 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.
>>>
>>> _______________________________________________
>>> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200518/d88a621b/attachment.html>