Corrispondente Curry-Howard della doppia negazione ((a-> r) -> r) o ((a-> ⊥) -> ⊥)?

Question

Quale è il corrispondente Curry-Howard della doppia negazione di a; (a -> r) -> r o (a -> ⊥) -> ⊥ o entrambi?

Entrambi i tipi possono essere codificati in Haskell come segue, dove ⊥ è codificato come forall b. b.

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

carta da Wadler 2003 nonché implementation in Haskell sembrano adottare precedente, mentre alcuni altra letteratura (ad esempio this) sembra sostenere quest'ultimo.

La mia attuale comprensione è che quest'ultimo è corretto. Ho difficoltà a capire l'ex stile, dal momento che è possibile creare un valore di tipo a da forall r. ((a -> r) -> r) utilizzando calcolo puro:

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

che sembra contraddire con la logica intuizionista che non si può derivare da a￢￢a.

Quindi, la mia domanda è: possibile p1 e p2 essere entrambi considerati corrispondenti Curry-Howard di ￢￢a? In tal caso, in che modo il fatto che siamo in grado di costruire p1 id :: a interagisce con la logica intuizionista?

---

Ho trovato una codifica più chiara della conversione da/a doppia negazione, per comodità di discussione. Grazie a @ 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

Per costruire un valore di tipo T1 a = forall r . (a -> r) -> r è almeno altrettanto impegnativo come la costruzione di un valore di tipo T2 a = (a -> Void) -> Void per, diciamo, Void ~ forall a . a.Questo può essere visto molto facilmente perché se siamo in grado di costruire un valore di tipo T1 a abbiamo automaticamente un valore al tipo T2 a semplicemente istanziando lo forall con Void.

D'altra parte, se abbiamo un valore di tipo T2 a non possiamo tornare indietro. Viene visualizzato il seguente circa la destra

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

ma non può essere il foro _ :: (a -> r) -> (a -> Void) piena di entrambi "sappiamo" nulla di r in questo contesto, e sappiamo che non possiamo costruire un Void.

---

Ecco un'altra differenza importante: T1 a -> a è abbastanza banale per codificare, istanziamo il forall con a e quindi applicare id

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

Ma, d'altra parte, non possiamo fare questo per T2 a

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

o, almeno non possiamo, senza barare il nostro intuizionista logica.

---

Così, insieme questi dovrebbe darci un indizio su quale dei T1 e T2 è genuina doppia negazione e perché ciascuno è utilizzato. Per essere chiari, T2 è davvero doppia negazione --- proprio come ci si aspetta --- ma T1 è più facile da gestire ... soprattutto se si lavora con Haskell98 che non ha tipi di dati null e tipi di rango più alti. Senza questi, l'unica codifica "valido" di Void è

newtype Void = Void Void 

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

che potrebbe non essere la cosa migliore per introdurre se non ne hai bisogno. Quindi, cosa garantisce che possiamo usare T1? Bene, finché consideriamo solo il codice che non è autorizzato a creare un'istanza di r con una variabile di tipo specifica, in effetti, stiamo agendo come se fosse un tipo astratto o esistenziale senza operazioni. Questo è sufficiente per gestire molti argomenti relativi alla doppia negazione (o continuazione) e quindi potrebbe essere più semplice parlare delle proprietà di forall r . (a -> r) -> r piuttosto che di (a -> Void) -> Void a patto che si mantenga una disciplina adeguata che permetta di convertire il primo in quest'ultimo se davvero necessario.

Answer 2

Lei ha ragione che (a -> r) -> r è una codifica corretta di doppia negazione secondo l'isomorfismo di Curry-Howard. Tuttavia, il tipo di funzione non si adatta a quel tipo! Il seguente:

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

dà un errore di tipo:

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) 

---

Più particolare: Non importa come si codifica in basso. Una breve demo in agda può aiutare a dimostrarlo. Supponendo solo un assioma - ovvero ex falso quodlibet, letteralmente "da falso tutto segue".

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) 

Nota non è possibile scrivere una definizione valida di doppio neg senza spegnere il controllo di terminazione (che è barare!). Se si tenta di nuovo la sua definizione, si ottiene anche un errore di tipo:

data ⊤ : Set where t : ⊤ 

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

dà

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

Qui !=< significa "non è un sottotipo di".

Answer 3

Per riassumere, l'approccio p2/T2 è più disciplinato, ma non possiamo ricavarne alcun valore pratico. D'altra parte p1/T1 consente di istanziare r, ma l'istanziazione è necessaria per eseguire runCont :: Cont r a -> (a -> r) -> r o runContT e ottenere qualsiasi risultato ed effetto collaterale di esso.

Tuttavia, siamo in grado di emulare il p2/T2 entro Control.Monad.Cont, istanziando r a Void, e utilizzando solo l'effetto collaterale, come segue:

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

-} 

Se vogliamo ulteriormente sbarazzarsi del brutto undefined :: Bottom , Penso di dover evitare la reinvenzione e utilizzare le librerie CPS come conduit e macchine.Un esempio di utilizzo machines è la seguente:

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

Grazie alla nostra conversazione, ora ho una migliore comprensione della firma tipo di runPlanT.