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

[Ruben Astudillo]

Hello cafe

I've been doing some basic logic exercises on Haskell the last few days.
Along the way I learned about intuitionistic logic and double negation.
On STLC types are propositions and terms of those types are proofs of
those propositions. The standard way to negate a proposition/type ~A~ in
Haskell is via the type

    type Not a = a -> Void

So far so good. On classical logic we have an equivalence between a
proposition and it's double negation. On intuitionistic logic I only
have a single implication that ~forall a. a -> Not (Not a)~, this is
easy to see as we have the proof/term

    proof :: forall a. a -> Not (Not a)
    proof a = \cont -> cont a

But we don't have the implication between ~forall a. Not (Not a) -> a~,
there is no way to obtain an ~a~ from the void continuations. Worse than
that, to even use such continuation I would need to have an ~a~ already.

On blogposts I've seen the claim that the types ~Void~ and ~forall a. a~
are almost the same. I can see the second one only has bottom as a term.
H98 versions of Void also had that term. The curious fact is that people
treat them as if they were the same without questioning.

But they are not the same, we can see this as there is an implication
~(forall r. (a -> r) -> r) -> a~ given by the proof

    proof1 :: forall a. (forall r. (a -> r) -> r) -> a
    proof1 cont = cont id

That leads me to believe that given that ~(forall r. (a -> r) -> r)~ and
~(a -> Void) -> Void)~ are not obviously the same, the relationship
between ~Void~ and ~forall a. a~ is not as people say.

So cafe, how can I reconcile these facts?

-- 
-- 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/20200513/08b2e18f/attachment.sig>