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

Brag

⊥ is not a type. You want Void as in en.wikibooks.org/wiki/Haskell/…. – Harrietharriett

@ReinHenrichs, I don't think it's at all unusual to call the empty type ⊥. It is the "bottom" of the lattice of types. – Waist

@Waist You're right of course. I'm just used to seeing it in a value context. – Harrietharriett

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.

Auditorium

I'd like to thank you especially for pointing out that we can instantiate r with Void . This helped me understand that T1 is stronger encoding than T2, and helped me construct the "fairy tale" semantics of double negation :) – Brag

Is it instantiating "forall with Void" or "forall r with Void" ? – Smtih

"forall" is just a binding and since the name r is ultimately only locally meaningful I try to not refer to it. It's the same way you apply functions f not functions f x = .... – Auditorium

newtype Void = Void Void would let a value exist: fix Void. – Sporadic

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".

Chappelka

The existence and mechanism of from_double_neg here is a strong indicator that forall r. (a -> r) -> r is not genuinely an encoding of double negation. – Auditorium

I'd like to thank user2407038 for clearing out the issue and Abrahamson for filling the comment in behalf of me! My current understanding is from_double_neg breaks the encoding because it instantiates r. And the p1/T1 encoding is unfortunate, if not wrong, in that Haskell has no mechanism to prevent instantiation of r. – Brag

Answer 3

To summarize, the approach p2/T2 is more disciplined, but we cannot compute any practical value out of it. On the other hand p1/T1 allows to instantiate r, but the instantiation is necessary to perform runCont :: Cont r a -> (a -> r) -> r or runContT and get any result and side effect out of it.

However, we can emulate p2/T2 within Control.Monad.Cont , by instantiating r to Void, and by using only the side effect, as follows:

{-# LANGUAGE RankNTypes #-}
import Control.Monad.Cont
import Control.Monad.Trans (lift)
import Control.Monad.Writer

newtype Bottom = Bottom { unleash :: forall a. a}

type C = ContT Bottom
type M = C (Writer String)

data USD1G = USD1G deriving Show

say x = lift $ tell $ x ++ "\n"

runM :: M a -> String
runM m = execWriter $
  runContT m (const $ return undefined) >> return ()
-- Are we sure that (undefined :: Bottom) above will never be used?

exmid :: M (Either USD1G (USD1G -> M Bottom))
exmid = callCC f
  where
     f k = return (Right (\x -> k (Left x)))

useTheWish :: Either USD1G (USD1G -> M Bottom) -> M ()
useTheWish e = case e of
  Left money -> say $ "I got money:" ++ show money
  Right method -> do
    say "I will pay devil the money."
    unobtainium <- method USD1G
    say $ "I am now omnipotent! The answer to everything is:"
      ++ show (unleash unobtainium :: Integer)

theStory :: String
theStory = runM $ exmid >>= useTheWish

main :: IO ()
main = putStrLn theStory

{-
> runhaskell bottom-encoding-monad.hs
I will pay devil the money.
I got money:USD1G

-}

If we want to further get rid of the ugly undefined :: Bottom , I think I need to avoid re-invention and use the CPS libraries such as conduits and machines. An example using machines is as follows:

{-# LANGUAGE RankNTypes, ImpredicativeTypes, ScopedTypeVariables #-}
import Data.Machine
import Data.Void
import Unsafe.Coerce

type M k a = Plan k String a
type PT k m a = PlanT k String m a

data USD = USD1G deriving (Show)

type Contract k m = Either USD (USD -> PT k m Void)

callCC :: forall a m k. ((a -> PT k m Void) -> PT k m a) -> PT k m a
callCC f = PlanT $
    \ kp ke kr kf ->
     runPlanT (f (\x -> PlanT $ \_ _ _ _ -> unsafeCoerce $kp x))
     kp ke kr kf

exmid ::  PT k m (Contract k m)
exmid = callCC f
  where
    f k =
       return $ Right (\x -> k (Left x))

planA :: Contract k m -> PT k m ()
planA e = case e of
  Left money ->
    yield $ "I got money: " ++ show money
  Right method -> do
    yield $ "I pay devil the money"
    u <- method USD1G
    yield $ "The answer to everything is :" ++ show (absurd u :: Integer)

helloMachine :: Monad m => SourceT m String
helloMachine = construct $ exmid >>= planA

main :: IO ()
main = do
  xs <- runT helloMachine
  print xs

Thanks to our conversation, now I have better understanding of the type signature of runPlanT .

Brag