haskell - ¿Es Curry-Howard corresponsal de doble negación((a-> r)-> r) o((a-> ⊥)-> ⊥)?

continuations

Question

Que es el corresponsal de Curry-Howard de la doble negación de a ; (a -> r) -> r o (a -> ⊥) -> ⊥ , o ambos?

Ambos tipos pueden codificarse en Haskell de la siguiente manera, donde ⊥ se codifica como para todos forall b. b forall b. b .

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

El documento de Wadler 2003 , así como la implementación en Haskell, parecen adoptar el primero, mientras que otra literatura (por ejemplo, this ) parece apoyar el segundo.

Mi entendimiento actual es que este último es correcto. Tengo dificultades para entender el estilo anterior, ya que puede crear un valor de tipo a de forall r. ((a -> r) -> r) forall r. ((a -> r) -> r) usando el cálculo puro:

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

lo que parece contradecir con la lógica intuicionista que no se puede derivar de ￢￢a .

Entonces, mi pregunta es: ¿pueden p1 y p2 ser considerados como corresponsales de Curry-Howard de ￢￢a ? Si es así, ¿cómo interactúa con la lógica intuicionista el hecho de que podamos construir p1 id :: a ?

He desarrollado una codificación más clara de la conversión a / desde la doble negación, para mayor comodidad de discusión. Gracias 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

Para construir un valor de tipo T1 a = forall r . (a -> r) -> r T1 a = forall r . (a -> r) -> r es al menos tan exigente como la construcción de un valor de tipo T2 a = (a -> Void) -> Void para, por ejemplo, Void ~ forall a . a Void ~ forall a . a Esto se puede ver con bastante facilidad porque si podemos construir un valor de tipo T1 a entonces automáticamente tenemos un valor en el tipo T2 a simplemente mediante la creación de una instancia del forall con Void .

Por otro lado, si tenemos un valor de tipo T2 a no podemos retroceder. Lo siguiente aparece sobre el derecho.

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

pero el agujero _ :: (a -> r) -> (a -> Void) no se puede rellenar: ambos "no sabemos" nada acerca de r en este contexto y sabemos que no podemos construir un Void .

Aquí hay otra diferencia importante: T1 a -> a es bastante trivial de codificar, creamos una instancia del forall con a y luego aplicamos el id

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

Pero, por otro lado, no podemos hacer esto para T2 a

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

O, al menos, no podemos sin engañar a nuestra lógica intuicionista.

Entonces, juntos deberían darnos una pista sobre cuál de T1 y T2 es la negación doble genuina y por qué se usa cada uno. Para ser claros, T2 es realmente una negación doble, como usted espera, pero es más fácil lidiar con T1 ... especialmente si trabaja con Haskell98, que carece de tipos de datos de nulo y de rango superior. Sin estos, la única codificación "válida" de Void es

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

lo que podría no ser lo mejor para presentar si no lo necesita. Entonces, ¿qué garantiza que podamos usar T1 lugar? Bueno, siempre y cuando solo consideremos un código que no está autorizado para instanciar r con una variable de tipo específica, entonces, en efecto, estamos actuando como si fuera un tipo abstracto o existencial sin operaciones. Esto es suficiente para manejar muchos argumentos relacionados con la doble negación (o continuaciones) y, por lo tanto, podría ser más sencillo hablar de las propiedades de forall r . (a -> r) -> r forall r . (a -> r) -> r lugar de (a -> Void) -> Void siempre y cuando mantenga una disciplina adecuada que le permita convertir el primero en el segundo si es realmente necesario.

Answer 2

Para resumir, el enfoque p2 / T2 es más disciplinado, pero no podemos calcular ningún valor práctico a partir de él. Por otro lado, p1 / T1 permite crear una instancia de r , pero la runCont :: Cont ra -> (a -> r) -> r instancias es necesaria para ejecutar runCont :: Cont ra -> (a -> r) -> r o runContT y obtener cualquier resultado y efecto secundario.

Sin embargo, podemos emular p2 / T2 dentro de Control.Monad.Cont , al crear una instancia de r en Void , y usar solo el efecto secundario, de la siguiente manera:

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

Si queremos deshacernos más de lo feo e undefined :: Bottom , creo que necesito evitar volver a inventar y usar las bibliotecas de CPS, como conductos y máquinas. Un ejemplo de uso de machines es el siguiente:

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

Gracias a nuestra conversación, ahora tengo una mejor comprensión de la firma de tipo de runPlanT .

Answer 3

Tienes razón en que (a -> r) -> r es una codificación correcta de doble negación según el isomorfismo de Curry-Howard. Sin embargo, el tipo de su función no se ajusta a ese tipo! El seguimiento:

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

da un error de 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)

Más detalle: No importa cómo codifiques el fondo. Una breve demostración en agda puede ayudar a mostrar esto. Suponiendo que solo hay un axioma, es decir, ex falso quodlibet , literalmente "de lo falso se sigue"

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)

Tenga en cuenta que no puede escribir una definición válida de doble neg sin desactivar el comprobador de terminación (que es trampa). Si vuelves a intentar tu definición, también obtendrás un error de tipo:

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

da

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

Aquí !=< Significa "no es un subtipo de".