Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)
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
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
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.
participants (2)
-
David Feuer -
Ruben Astudillo