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

[Ruben Astudillo]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200517/0cd025e2/attachment.sig>