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

[David Feuer]

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 we'd normally write something like

  forall r. (forall q. a -> q) -> r

On Wed, May 13, 2020, 1:36 AM Ruben Astudillo <ruben.astud at gmail.com> wrote:

> 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200513/cfae1ef6/attachment.html>