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

Ruben Astudillo ruben.astud at gmail.com
Wed May 13 05:35:52 UTC 2020

```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

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?

--