Ist Curry-Howard Korrespondent der doppelten Negation ((a-> r) -> r) oder ((a-> ∞) -> ⊥)?

Question

Welches ist der Curry-Howard-Korrespondent der doppelten Verneinung von a; (a -> r) -> r oder (a -> ⊥) -> ⊥, oder beides?

Beide Typen können in Haskell wie folgt codiert werden, wobei ⊥ als forall b. b codiert ist.

p1 :: forall r. ((a -> r) -> r) 
p2 :: (a -> (forall b. b)) -> (forall b. b) 

Papier von Wadler 2003 sowie implementation in Haskell scheinen die ersteren zu verabschieden, während einige andere Literatur (z this) diese zu unterstützen scheint.

Mein derzeitiges Verständnis ist, dass letzteres korrekt ist. Ich habe Schwierigkeiten, den ehemaligen Stil zu verstehen, da Sie a von forall r. ((a -> r) -> r) mit reiner Berechnung einen Wert vom Typ erstellen:

> let p1 = ($42) :: forall r. (Int -> r) -> r 
> p1 id 
42 

, die mit intuitionismus zu widersprechen scheinen, dass Sie nicht a von ￢￢a ableiten können.

Also, meine Frage ist: können p1 und p2 beide als Curry-Howard Korrespondent von ￢￢a betrachtet werden? Wenn ja, wie interagiert die Tatsache, dass wir p1 id :: a konstruieren können, mit der intuitionistischen Logik?

---

Ich habe mit klarer Codierung der Umwandlung in/aus doppelter Negation, zur Erleichterung der Diskussion kommen. Danke an @ 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

Um einen Wert vom Typ T1 a = forall r . (a -> r) -> r zu konstruieren, ist mindestens so anspruchsvoll wie die Konstruktion eines Wertes vom Typ T2 a = (a -> Void) -> Void für, sagen wir, Void ~ forall a . a.Das kann ziemlich einfach gesehen werden, denn wenn wir einen Wert vom Typ T1 a konstruieren können, haben wir automatisch einen Wert vom Typ T2 a, indem wir einfach forall mit Void instanziieren.

Auf der anderen Seite, wenn wir einen Wert vom Typ T2 a haben, können wir nicht zurückgehen. Im Folgenden wird über rechts

dne :: forall a . ((a -> Void) -> Void) -> (forall r . (a -> r) -> r) 
dne t2 = \f -> absurd (t2 (_ f)) -- we cannot fill _ 

aber das Loch _ :: (a -> r) -> (a -> Void) nicht sein kann ausgefüllt wir beide „wissen“ nichts über r in diesem Zusammenhang, und wir wissen, dass wir nicht ein Void konstruieren können.

---

Hier ist ein weiterer wichtiger Unterschied: T1 a -> a zu kodieren ziemlich trivial ist, instanziiert wir die forall mit a und gelten dann id

project :: T1 a -> a 
project t1 = t1 id 

Aber auf der anderen Seite, können wir dies nicht tun, für T2 a

projectX :: T2 a -> a 
projectX t2 = absurd (t2 (_ :: a -> Void)) 

oder zumindest können wir nicht ohne unser intuitionistic betrügen Logik.

---

Also, zusammen diese sollten uns einen Hinweis geben, wie auf die von T1 und T2 echte doppelte Verneinung ist und warum jeder verwendet wird. Um klar zu sein, ist T2 wirklich doppelte Verneinung --- genau wie Sie erwarten --- aber T1 ist leichter zu behandeln ... vor allem, wenn Sie mit Haskell98 arbeiten, die Nullwert-Datentypen und höhere Rank-Typen fehlt. Ohne diese ist die einzige „gültig“ Codierung von Void

newtype Void = Void Void 

absurd :: Void -> a 
absurd (Void v) = absurd v 

, die nicht das Beste, was sein könnte vorstellen, wenn Sie es nicht brauchen. Also, was stellt sicher, dass wir stattdessen T1 verwenden können? Nun, solange wir nur Code betrachten, der r mit einer spezifischen Typvariablen nicht instanziieren darf, verhalten wir uns tatsächlich so, als ob es ein abstrakter oder existenzieller Typ ohne Operationen wäre. Dies ist ausreichend für die Behandlung vieler Argumente in Bezug auf doppelte Negation (oder Fortsetzungen) und so könnte es einfacher sein, nur über die Eigenschaften von forall r . (a -> r) -> r statt (a -> Void) -> Void zu sprechen, solange Sie eine ordnungsgemäße Disziplin, die Sie die erstere zu letzterem konvertieren können pflegen wenn wirklich benötigt.

Answer 2

Sie sind richtig, dass (a -> r) -> r ist eine richtige Codierung der doppelten Negation nach dem Curry-Howard Isomorphismus. Der Typ Ihrer Funktion passt jedoch nicht zu diesem Typ! Die folgende:

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

gibt einen Typfehler:

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) 

---

Mehr Detail: Es spielt keine Rolle, wie Sie unten kodieren. Eine kurze Demo in agda kann dies zeigen. Angenommen, nur ein Axiom - nämlich ex falso quodlibet, buchstäblich "aus false alles folgt".

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) 

Hinweis: Sie können keine gültige Definition von double-neg ohne Ausschalten die Abschlussprüfung (das ist Betrug!) Schreiben. Wenn Sie Ihre Definition versuchen Sie es erneut, erhalten Sie auch eine Art Fehler:

data ⊤ : Set where t : ⊤ 

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

gibt

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

Hier !=< Mittel „ist kein Subtyp von“.

Answer 3

Zusammenfassend ist der Ansatz p2/T2 disziplinierter, aber wir können keinen praktischen Wert daraus berechnen. Auf der anderen Seite ermöglicht p1/T1 die Instantiierung r, aber die Instanziierung ist notwendig, um runCont :: Cont r a -> (a -> r) -> r oder runContT durchzuführen und irgendein Ergebnis und Nebeneffekt daraus zu erhalten.

können wir jedoch p2/T2 innerhalb Control.Monad.Cont, emulieren, indem r zu Void instanziiert wird, und nur durch die Nebenwirkung wie folgt verwendet:

{-# 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 

-} 

Wenn wir weiter von der hässlichen undefined :: Bottom loswerden wollen Ich denke, ich muss vermeiden, dass ich die CPS-Bibliotheken wie Conduits und Maschinen neu erfinde und benutze.Ein Beispiel machines ist wie folgt:

{-# 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 

Dank unserem Gespräch, jetzt habe ich ein besseres Verständnis der Art Signatur von runPlanT haben.