[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
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
More information about the Haskell-Cafe
mailing list