title: Is Curry-Howard correspondent of double negation ((a->r)->r) or ((a->⊥)->⊥)?
body: <p>Which is the Curry-Howard correspondent of double negation of <code>a</code>; <code>(a -&gt; r) -&gt; r</code> or <code>(a -&gt; ⊥) -&gt; ⊥</code>, or both? </p>
  
  <p>Both types can be encoded in Haskell as follows, where <code>⊥</code> is encoded as <code>forall b. b</code>.</p>
  
  <pre class="lang-hs prettyprint-override"><code>p1 :: forall r. ((a -&gt; r) -&gt; r)
  p2 :: (a -&gt; (forall b. b)) -&gt; (forall b. b)
  </code></pre>
  
  <p>Paper by <a href="http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf" rel="noreferrer">Wadler 2003</a> as well as 
  <a href="https://hackage.haskell.org/package/mtl-2.2.1/docs/Control-Monad-Cont.html#v:cont" rel="noreferrer">implementation in Haskell</a> seem to adopt the former, while some 
  other literature (e.g. <a href="http://www.lix.polytechnique.fr/~lengrand/Work/Teaching/MPRI/lecture1.pdf" rel="noreferrer">this</a>) seems to support the latter.</p>
  
  <p>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 <code>a</code> from <code>forall r. ((a -&gt; r) -&gt; r)</code> using pure computation:</p>
  
  <pre class="lang-hs prettyprint-override"><code>&gt; let p1 = ($42) :: forall r. (Int -&gt; r) -&gt; r
  &gt; p1 id
  42
  </code></pre>
  
  <p>which seems to contradict with intuitionistic logic that you cannot derive <code>a</code> from <code>￢￢a</code>. </p>
  
  <p>So, my question is: can <code>p1</code> and <code>p2</code> both be regarded as Curry-Howard correspondent of  <code>￢￢a</code> ? If so, how does the fact that we can construct <code>p1 id :: a</code> interact with the intuitionistic logic?</p>
  
  <hr>
  
  <p>I have come up with clearer encoding of conversion to/from double negation, for convenience of discussion. Thanks to @user2407038 !</p>
  
  <pre><code>{-# LANGUAGE RankNTypes #-}
  to_double_neg :: forall a. a -&gt; (forall r. (a-&gt;r)-&gt;r)
  to_double_neg x = ($x)
  
  from_double_neg :: forall a. (forall r. (a-&gt;r)-&gt;r) -&gt; a
  from_double_neg x = x id
  </code></pre>