[Haskell-cafe] Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)
David Feuer
david.feuer at gmail.com
Wed May 13 05:44:42 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 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>
More information about the Haskell-Cafe
mailing list