Is Curry-Howard correspondent of double negation ((a->r)->r) or ((a->⊥)->⊥)?

Question

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

Answer 1

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.

Answer 2

You are correct that (a -> r) -> r is a correct encoding of double negation according to the Curry-Howard isomorphism. However, the type of your function does not fit that type! The following:

double_neg :: forall a r . ((a -> r) -> r)
double_neg = (($42) :: (Int -> r) -> r ) 

gives a type error:

Couldn't match type `a' with `Int'
      `a' is a rigid type variable bound by
          the type signature for double_neg :: (a -> r) -> r at test.hs:20:22
    Expected type: (a -> r) -> r
      Actual type: (Int -> r) -> r
    Relevant bindings include
      double_neg :: (a -> r) -> r (bound at test.hs:21:1)

---

More detail: It doesn't matter how you encode bottom. A short demo in agda can help show this. Assuming only one axiom - namely ex falso quodlibet, literally "from false anything follows".

record Double-Neg : Set₁ where
  field 
    ⊥ : Set
    absurd : {A : Set} → ⊥ → A

  ¬_ : Set → Set
  ¬ A = A → ⊥ 

  {-# NO_TERMINATION_CHECK #-}
  double-neg : { P : Set } → ¬ (¬ P) → P
  double-neg f = absurd r where r = f (λ _ → r)

Note you cannot write a valid definition of double-neg without turning off the termination checker (which is cheating!). If you try your definition again, you also get a type error:

  data ⊤ : Set where t : ⊤

  double-neg : { P : Set } → ¬ (¬ P) → P
  double-neg {P} f = f t 

gives

⊤ !=< (P → ⊥)
when checking that the expression t has type ¬ P

Here !=< means "is not a subtype of".