¿Hay alguna manera de realizar una función de tipo ((a -> b) -> b) -> O ab?

Propuestas (P -> Q) -> Qy P \/ Qson equivalentes.

¿Hay alguna manera de presenciar esta equivalencia en Haskell?

from :: Either a b -> ((a -> b) -> b)
from x = case x of
         Left a -> \f -> f a
         Right b -> \f -> b

to :: ((a -> b) -> b) -> Either a b
to = ???

tal que

from . to = idy to . from = id?

Propuestas (P -> Q) -> Qy P \/ Qson equivalentes.

Esto es cierto en la lógica clásica, pero no en la lógica constructiva.

En la lógica constructiva no tenemos la ley del medio excluido , es decir, no podemos comenzar a pensar con "o P es verdadero o P no es verdadero".

Clásicamente razonamos como:

• si P es verdadero (es decir, tenemos ( x :: P)), entonces devuelve Left x.
• si P es falso, entonces en Haskell hablar tendríamos nx :: P -> Voidfunción. Luego absurd . nx :: P -> Q(podemos alcanzar cualquier tipo de pico, tomamos Q) y llamar dado f :: (P -> Q) -> Q)con absurd . nxpara obtener el valor de tipo Q.

El problema es que no hay una función general de un tipo:

lem :: forall p. Either p (p -> Void)

Para algunos tipos concretos hay, por ejemplo, Boolestá habitada para que podamos escribir

lemBool :: Either Bool (Bool -> Void)
lemBool = Left True -- arbitrary choice

pero de nuevo, en general no podemos.

No, es imposible Considere el caso especial donde Q = Void.

Either P Qes entonces Either P Void, que es isomorfo a P.

iso :: P -> Either P Void
iso = Left

iso_inv :: Either P Void -> P
iso_inv (Left p)  = p
iso_inv (Right q) = absurd q

Por lo tanto, si tuviéramos un término de función

impossible :: ((P -> Void) -> Void) -> Either P Void

también podríamos tener un término

impossible2 :: ((P -> Void) -> Void) -> P
impossible2 = iso_inv . impossible

Según la correspondencia de Curry-Howard, esto sería una tautología en la lógica intuicionista :

((P -> False) -> False) -> P

Pero lo anterior es la eliminación de la doble negación, que es bien sabido que es imposible de probar en la lógica intuicionista , de ahí una contradicción. (El hecho de que podamos probarlo en la lógica clásica no es relevante).

(Nota final: esto supone que nuestro programa Haskell finalizará. Por supuesto, usando la recursión infinita undefinedy formas similares para evitar devolver un resultado, podemos habitar cualquier tipo en Haskell).

No, no es posible, pero es un poco sutil. El problema es que las variables de tipo ay bestán universalmente cuantificadas.

to :: ((a -> b) -> b) -> Either a b
to f = ...

ay bestán universalmente cuantificados. La persona que llama elige qué tipo son, por lo que no puede simplemente crear un valor de cualquier tipo. Esto implica que no puede simplemente crear un valor de tipo Either a bmientras ignora el argumento f. Pero usar ftambién es imposible. Sin saber qué tipos ay qué bson, no puede crear un valor de tipo a -> bpara pasar f. Simplemente no hay suficiente información disponible cuando los tipos se cuantifican universalmente.

En cuanto a por qué el isomorfismo no funciona en Haskell, ¿estás seguro de que esas proposiciones son equivalentes en una lógica constructivista intuicionista? Haskell no implementa una lógica deductiva clásica.

Como otros han señalado, esto es imposible porque no tenemos la ley del medio excluido. Déjame pasar por eso un poco más explícitamente. Supongamos que tenemos

bogus :: ((a -> b) -> b) -> Either a b

y nos propusimos b ~ Void. Entonces tenemos

-- chi calls this `impossible2`.
double_neg_elim :: ((a -> Void) -> Void) -> a
bouble_neg_elim f = case bogus f of
             Left a -> a
             Right v -> absurd v

Ahora, demostremos la doble negación de la ley del medio excluido aplicada a una proposición específica .

nnlem :: forall a. (Either a (a -> Void) -> Void) -> Void
nnlem f = not_not_a not_a
  where
    not_a :: a -> Void
    not_a = f . Left

    not_not_a :: (a -> Void) -> Void
    not_not_a = f . Right

Y ahora

lem :: Either a (a -> Void)
lem = double_neg_elim nnlem

lemclaramente no puede existir porque apuede codificar la proposición de que cualquier configuración de máquina de Turing que elija se detendrá.

Verifiquemos que lemsea ​​suficiente:

bogus :: forall a b. ((a -> b) -> b) -> Either a b
bogus f = case lem @a of
  Left a -> Left a
  Right na -> Right $ f (absurd . na)

No tengo idea de si esto es válido en términos de lógica, o qué significa para su equivalencia, pero sí, es posible escribir dicha función en Haskell.

Para construir un Either a b, necesitamos un ao un bvalor. No tenemos ninguna forma de construir un avalor, pero tenemos una función que devuelve un valor bque podríamos llamar. Para hacer eso, necesitamos proporcionar una función que convierta un aen a b, pero dado que los tipos son desconocidos, en el mejor de los casos podríamos hacer una función que devuelva una constante b. Para obtener ese bvalor, no podemos construirlo de otra manera que antes, por lo que esto se convierte en un razonamiento circular, y podemos resolverlo simplemente creando un punto de fijación :

to :: ((a -> b) -> b) -> Either a b
to f = let x = f (\_ -> x) in Right x