<div dir="auto"><div>You're misplacing your quantifiers.</div><div dir="auto"><br></div><div dir="auto"><span style="font-family:sans-serif">  (a -> Void) -> Void)</span></div><div dir="auto"><font face="sans-serif"><br></font></div><div dir="auto"><font face="sans-serif">is not isomorphic to</font></div><div dir="auto"><font face="sans-serif"><br></font></div><div dir="auto"><span style="font-family:sans-serif">  forall r. (a -> r) -> r</span></div><div dir="auto"><font face="sans-serif"><br></font></div><div dir="auto"><font face="sans-serif">but *is* isomorphic to</font></div><div dir="auto"><font face="sans-serif"><br></font></div><div dir="auto"><font face="sans-serif">  (a -> (forall r. r)) -> (forall r. r)</font></div><div dir="auto"><font face="sans-serif"><br></font></div><div dir="auto"><font face="sans-serif">which we'd normally write something like</font></div><div dir="auto"><font face="sans-serif"><br></font></div><div dir="auto"><font face="sans-serif">  forall r. (forall q. a -> q) -> r</font></div><div dir="auto"><br><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Wed, May 13, 2020, 1:36 AM Ruben Astudillo <<a href="mailto:ruben.astud@gmail.com">ruben.astud@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello cafe<br>
<br>
I've been doing some basic logic exercises on Haskell the last few days.<br>
Along the way I learned about intuitionistic logic and double negation.<br>
On STLC types are propositions and terms of those types are proofs of<br>
those propositions. The standard way to negate a proposition/type ~A~ in<br>
Haskell is via the type<br>
<br>
    type Not a = a -> Void<br>
<br>
So far so good. On classical logic we have an equivalence between a<br>
proposition and it's double negation. On intuitionistic logic I only<br>
have a single implication that ~forall a. a -> Not (Not a)~, this is<br>
easy to see as we have the proof/term<br>
<br>
    proof :: forall a. a -> Not (Not a)<br>
    proof a = \cont -> cont a<br>
<br>
But we don't have the implication between ~forall a. Not (Not a) -> a~,<br>
there is no way to obtain an ~a~ from the void continuations. Worse than<br>
that, to even use such continuation I would need to have an ~a~ already.<br>
<br>
On blogposts I've seen the claim that the types ~Void~ and ~forall a. a~<br>
are almost the same. I can see the second one only has bottom as a term.<br>
H98 versions of Void also had that term. The curious fact is that people<br>
treat them as if they were the same without questioning.<br>
<br>
But they are not the same, we can see this as there is an implication<br>
~(forall r. (a -> r) -> r) -> a~ given by the proof<br>
<br>
    proof1 :: forall a. (forall r. (a -> r) -> r) -> a<br>
    proof1 cont = cont id<br>
<br>
That leads me to believe that given that ~(forall r. (a -> r) -> r)~ and<br>
~(a -> Void) -> Void)~ are not obviously the same, the relationship<br>
between ~Void~ and ~forall a. a~ is not as people say.<br>
<br>
So cafe, how can I reconcile these facts?<br>
<br>
-- <br>
-- Rubén<br>
-- pgp: 4EE9 28F7 932E F4AD<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div></div></div>