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

[Olaf Klinke]

> You're misplacing your quantifiers.
> 
>   (a -> Void) -> Void)
> 
> is not isomorphic to
> 
>   forall r. (a -> r) -> r
> 
> but *is* isomorphic to
> 
>   (a -> (forall r. r)) -> (forall r. r)
> 
...which is because you could _define_ Void to be (forall r. r):
{-# LANGUAGE Rank2Types #-}
newtype Void = Void {absurd :: forall r. r}

In practice, Void used to be implemented as

data Void = Void Void

before it became just

data Void 

by means of EmptyDataDecls extension. The latter has the advantage that
there is no constructor named 'Void'. In reality of course, Void does
have an element, bottom, which it shares with all other types. Hence
the 'absurd' function that returns the bottom in type r when given the
bottom in type Void. But as you know the correspondence between types
and theorems in intuitionistic logic explicitly regards only total
values. 

Excersise: Prove that intuitionistically, it is absurd to deny the law
of excluded middle:

Not (Not (Either a (Not a)))

There is a whole world to be discovered beneath the total values. 
Think about the type () as truth values and what universal
quantification could be. 

Olaf