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

Olaf Klinke olf at aatal-apotheke.de
Wed May 13 13:15:15 UTC 2020

> 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

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. 


More information about the Haskell-Cafe mailing list