Which is the Curry-Howard correspondent of double negation of a; (a -> r) -> r or (a -> ⊥) -> ⊥, or both?
Both types can be encoded in Haskell as follows, where ⊥ is encoded as forall b. b.
p1 :: forall r. ((a -> r) -> r)
p2 :: (a -> (forall b. b)) -> (forall b. b)
Paper by Wadler 2003 as well as implementation in Haskell seem to adopt the former, while some other literature (e.g. this) seems to support the latter.
My current understanding is that the latter is correct. I have difficulty in understanding the former style, since you can create a value of type a from forall r. ((a -> r) -> r) using pure computation:
> let p1 = ($42) :: forall r. (Int -> r) -> r
> p1 id
42
which seems to contradict with intuitionistic logic that you cannot derive a from ￢￢a.
So, my question is: can p1 and p2 both be regarded as Curry-Howard correspondent of ￢￢a ? If so, how does the fact that we can construct p1 id :: a interact with the intuitionistic logic?
I have come up with clearer encoding of conversion to/from double negation, for convenience of discussion. Thanks to @user2407038 !
{-# LANGUAGE RankNTypes #-}
to_double_neg :: forall a. a -> (forall r. (a->r)->r)
to_double_neg x = ($x)
from_double_neg :: forall a. (forall r. (a->r)->r) -> a
from_double_neg x = x id
To construct a value of type T1 a = forall r . (a -> r) -> r is at least as demanding as construction of a value of type T2 a = (a -> Void) -> Void for, say, Void ~ forall a . a. This can be pretty easily seen because if we can construct a value of type T1 a then we automatically have a value at type T2 a by merely instantiating the forall with Void.
On the other hand, if we have a value of type T2 a we cannot go back. The following appears about right
dne :: forall a . ((a -> Void) -> Void) -> (forall r . (a -> r) -> r)
dne t2 = \f -> absurd (t2 (_ f)) -- we cannot fill _
but the hole _ :: (a -> r) -> (a -> Void) cannot be filled—we both "know" nothing about r in this context and we know we cannot construct a Void.
Here's another important difference: T1 a -> a is fairly trivial to encode, we instantiate the forall with a and then apply id
project :: T1 a -> a
project t1 = t1 id
But, on the other hand, we cannot do this for T2 a
projectX :: T2 a -> a
projectX t2 = absurd (t2 (_ :: a -> Void))
or, at least we cannot without cheating our intuitionistic logic.
So, together these ought to give us a hint as to which of T1 and T2 is genuine double negation and why each is used. To be clear, T2 is genuinely double negation---just like you expect---but T1 is easier to deal with... especially if you work with Haskell98 which lacks nullary data types and higher rank types. Without these, the only "valid" encoding of Void is
newtype Void = Void Void
absurd :: Void -> a
absurd (Void v) = absurd v
which might not be the best thing to introduce if you don't need it. So what ensures that we can use T1 instead? Well, as long as we only ever consider code which is not allowed to instantiate r with a specific type variable then we are, in effect, acting as though it is an abstract or existential type with no operations. This is sufficient for handling many arguments pertaining to double negation (or continuations) and so it might be simpler to just talk about the properties of forall r . (a -> r) -> r rather than (a -> Void) -> Void so long as you maintain a proper discipline which allows you to convert the former to the latter if genuinely needed.