plataforma - haskell uso

¿Tener un `(a-> b)-> b` equivale a tener un` a`?

Question

En un lenguaje funcional puro, lo único que puede hacer con un valor es aplicarle una función.

En otras palabras, si desea hacer algo interesante con un valor de tipo a , necesita una función (por ejemplo) con tipo f :: a -> b y luego aplíquela. Si alguien te entrega (flip apply) a con tipo (a -> b) -> b , ¿es un reemplazo adecuado para a ?

¿Y a qué llamarías algo con tipo (a -> b) -> b ? Viendo que parece ser un sustituto de una a , estaría tentado de llamarlo proxy, o algo de http://www.thesaurus.com/browse/proxy .

Answer 1

Esta pregunta es una ventana a una serie de conceptos más profundos.

Primero, tenga en cuenta que hay una ambigüedad en esta pregunta. ¿Nos referimos al tipo forall b. (a -> b) -> b forall b. (a -> b) -> b , de modo que podamos instanciar b con el tipo que queramos, o queremos decir (a -> b) -> b para alguna b específica que no podemos elegir.

Podemos formalizar esta distinción en Haskell así:

newtype Cont b a = Cont ((a -> b) -> b)
newtype Cod a    = Cod (forall b. (a -> b) -> b)

Aquí vemos un poco de vocabulario. El primer tipo es la mónada Cont , el segundo es la Identity Codensity , aunque mi familiaridad con este último término no es lo suficientemente fuerte como para decir lo que se debe llamar en inglés.

Cont ba no puede ser equivalente a a a menos que a -> b pueda contener al menos tanta información como a (vea el comentario de Dan Robertson a continuación). Entonces, por ejemplo, note que nunca puede sacar nada de Cont Void a .

Cod a es equivalente a a . Para ver esto es suficiente presenciar el isomorfismo:

toCod :: a -> Cod a
fromCod :: Cod a -> a

cuyas implementaciones dejaré como ejercicio. Si realmente quieres hacerlo, puedes intentar probar que este par realmente es un isomorfismo. fromCod . toCod = id fromCod . toCod = id es fácil, pero toCod . fromCod = id toCod . fromCod = id requiere el teorema libre para Cod .

Answer 2

La respuesta de luqui es excelente, pero voy a ofrecer otra explicación de forall b. (a -> b) -> b === a forall b. (a -> b) -> b === a por un par de razones: Primero, porque creo que la generalización de Codensity es un poco demasiado entusiasta. Y segundo, porque es una oportunidad para unir un montón de cosas interesantes. ¡Adelante!

caja mágica de z5h

Imagina que alguien arrojó una moneda y luego la puso en una caja mágica. No se puede ver dentro del cuadro, pero si elige un tipo b y le pasa una función con el tipo Bool -> b , el recuadro escupirá una b . ¿Qué podemos aprender sobre esta caja sin mirar dentro? ¿Podemos saber cuál es el estado de la moneda? ¿Podemos aprender qué mecanismo utiliza la caja para producir el b ? Como resultado, podemos hacer ambas cosas.

Podemos definir el cuadro como una función de rango 2 de tipo Box Bool donde

type Box a = forall b. (a -> b) -> b

(Aquí, el tipo de rango 2 significa que el creador de cajas elige a y el usuario de la caja elige b ).

Ponemos el a en la caja y luego cerramos la caja, creando ... un cierre .

-- Put the a in the box.
box :: a -> Box a
box a f = f a

Por ejemplo, box True . ¡La aplicación parcial es solo una forma inteligente de crear cierres!

Ahora, ¿es la moneda cara o cruz? Como yo, el usuario de la caja, puedo elegir b , puedo elegir Bool y pasar una función Bool -> Bool . Si elijo id :: Bool -> Bool entonces la pregunta es: ¿el cuadro escupirá el valor que contiene? La respuesta es que la caja escupirá el valor que contiene o escupirá tonterías (un valor inferior como undefined ). En otras palabras, si obtiene una respuesta, entonces esa respuesta debe ser correcta.

-- Get the a out of the box.
unbox :: Box a -> a
unbox f = f id

Debido a que no podemos generar valores arbitrarios en Haskell, la única cosa sensible que la caja puede hacer es aplicar la función dada al valor que está ocultando. Esto es una consecuencia del polimorfismo paramétrico, también conocido como parametricidad .

Ahora, para mostrar que Box a es isomorfo a a , debemos probar dos cosas sobre boxeo y desempaquetado. Necesitamos demostrar que sacas lo que pones y que puedes poner lo que obtienes.

unbox . box = id
box . unbox = id

Haré el primero y dejaré el segundo como ejercicio para el lector.

  unbox . box
= {- definition of (.) -}
  /b -> unbox (box b)
= {- definition of unbox and (f a) b = f a b -}
  /b -> box b id
= {- definition of box -}
  /b -> id b
= {- definition of id -}
  /b -> b
= {- definition of id, backwards -}
  id

(Si estas pruebas parecen más bien triviales, eso se debe a que todas las funciones polimórficas (totales) en Haskell son transformaciones naturales y lo que estamos demostrando aquí es la naturalidad. ¡La parametricidad una vez más nos proporciona teoremas para precios bajos y bajos!)

Como un aparte y otro ejercicio para el lector, ¿por qué no puedo definir rebox con (.) ?

rebox = box . unbox

¿Por qué tengo que poner en línea la definición de (.) mí mismo como una especie de persona de las cavernas?

rebox :: Box a -> Box a
rebox f = box (unbox f)

(Sugerencia: ¿cuáles son los tipos de box , unbox y (.) ?)

Identidad y Codensity y Yoneda, ¡Oh, Dios mío!

Ahora, ¿cómo podemos generalizar Box ? luqui usa Codensity : ambos b s son generalizados por un constructor de tipo arbitrario que llamaremos f . Esta es la transform de Codensity de fa .

type CodenseBox f a = forall b. (a -> f b) -> f b

Si arreglamos f ~ Identity , recuperamos Box . Sin embargo, hay otra opción: podemos presionar solo el tipo de retorno con f :

type YonedaBox f a = forall b. (a -> b) -> f b

(De alguna manera he regalado el juego aquí con este nombre pero volveremos sobre eso.) También podemos corregir f ~ Identity aquí para recuperar Box , pero dejamos que el usuario de la caja pase en una función normal en lugar de una Flecha de Kleisli Para entender lo que estamos generalizando, veamos nuevamente la definición de box :

box a f = f a

Bueno, esto es solo flip ($) , ¿no? Y resulta que nuestros otros dos cuadros se crean mediante la generalización ($) : CodenseBox es un enlace monádico invertido parcialmente aplicado, y YonedaBox es un YonedaBox parcialmente aplicado. (Esto también explica por qué Codensity f es una Monad y Yoneda f es un Functor para cualquier opción de f : la única forma de crear una es cerrando un bind o fmap, respectivamente.) Además, ambos conceptos de la teoría de categoría esotérica son realmente generalizaciones de un concepto que es familiar para muchos programadores que trabajan: ¡la transformación de CPS!

En otras palabras, YonedaBox es la Incrustación de Yoneda y las leyes de box / unbox debidamente abstractas para YonedaBox son la prueba del Yoneda Lemma.

TL; DR:

forall b. (a -> b) -> b === a forall b. (a -> b) -> b === a es una instancia del Yoneda Lemma.

Answer 3

Las otras respuestas han hecho un gran trabajo al describir la relación entre los tipos de todo forall b . (a -> b) -> b forall b . (a -> b) -> b y a pero me gustaría señalar una advertencia porque lleva a algunas preguntas abiertas interesantes en las que he estado trabajando.

Técnicamente, forall b . (a -> b) -> b forall b . (a -> b) -> b y a no son isomorfos en un lenguaje como Haskell que (1) le permite escribir una expresión que no termina y (2) es llamar por valor (estricto) o contiene seq . Mi punto aquí no es ser quisquilloso ni mostrar que la parametricidad se debilita en Haskell (como es bien sabido), pero que puede haber formas claras de fortalecerla y, en cierto sentido, reclamar isomorfismos como este.

Hay algunos términos de tipo forall b . (a -> b) -> b forall b . (a -> b) -> b que no se puede expresar como a . Para ver por qué, comencemos por mirar la prueba Rein left left a exercise, box . unbox = id box . unbox = id . Resulta que esta prueba es realmente más interesante que la de su respuesta, ya que depende de la parametricidad de una manera crucial.

box . unbox
= {- definition of (.) -}
  /m -> box (unbox m)
= {- definition of box -}
  /m f -> f (unbox m)
= {- definition of unbox -}
  /m f -> f (m id)
= {- free theorem: f (m id) = m f -}
  /m f -> m f
= {- eta: (/f -> m f) = m -}
  /m -> m
= {- definition of id, backwards -}
  id

El paso interesante, donde la parametricidad entra en juego, es la aplicación del teorema libre f (m id) = mf . Esta propiedad es una consecuencia de forall b . (a -> b) -> b forall b . (a -> b) -> b , el tipo de m . Si pensamos en m como una casilla con un valor subyacente de tipo a adentro, entonces lo único que m puede hacer con su argumento es aplicarlo a este valor subyacente y devolver el resultado. En el lado izquierdo, esto significa que f (m id) extrae el valor subyacente del cuadro y lo pasa a f . A la derecha, esto significa que m aplica f directamente al valor subyacente.

Lamentablemente, este razonamiento no se cumple cuando tenemos términos como m y f continuación.

m :: (Bool -> b) -> b
m k = seq (k true) (k false)

f :: Bool -> Int
f x = if x then ⊥ else 2`

Recordemos que queríamos mostrar f (m id) = mf

f (m id)
= {- definition f -}
  if (m id) then ⊥ else 2
= {- definition of m -}
  if (seq (id true) (id false)) then ⊥ else 2
= {- definition of id -}
  if (seq true (id false)) then ⊥ else 2
= {- definition of seq -}
  if (id false) then ⊥ else 2
= {- definition of id -}
  if false then ⊥ else 2
= {- definition of if -}
  2

m f
= {- definition of m -}
  seq (f true) (f false)
= {- definition of f -}
  seq (if true then ⊥ else 2) (f false)
= {- definition of if -}
  seq ⊥ (f false)
= {- definition of seq -}
  ⊥

Claramente, 2 no es igual a ⊥ así que hemos perdido nuestro teorema libre y el isomorfismo entre a y (a -> b) -> b con él. Pero, ¿qué pasó exactamente? Esencialmente, m no es solo una caja de buen comportamiento porque aplica su argumento a dos valores subyacentes diferentes (y utiliza seq para garantizar que ambas aplicaciones se evalúen realmente), lo que podemos observar al pasar en una continuación que termina en una de estos valores subyacentes, pero no el otro. En otras palabras, m id = false no es realmente una representación fiel de m como Bool porque ''olvida'' el hecho de que m llama a su entrada con true y false .

El problema es el resultado de la interacción entre tres cosas:

1. La presencia de la no determinación
2. La presencia de seq.
3. El hecho de que los términos de tipo para todo forall b . (a -> b) -> b forall b . (a -> b) -> b puede aplicar su entrada varias veces.

No hay mucha esperanza de superar los puntos 1 o 2. Sin embargo, los tipos lineales pueden darnos la oportunidad de combatir el tercer problema. Una función lineal de tipo a ⊸ b es una función de tipo a a tipo b que debe usar su entrada exactamente una vez. Si requerimos que m tenga el tipo forall b . (a -> b) ⊸ b forall b . (a -> b) ⊸ b , entonces esto descarta nuestro contraejemplo al teorema libre y debería permitirnos mostrar un isomorfismo entre a y forall b . (a -> b) ⊸ b forall b . (a -> b) ⊸ b incluso en presencia de no determinación y seq .

¡Esto es realmente genial! Muestra que la linealidad tiene la capacidad de ''rescatar'' propiedades interesantes mediante efectos de domesticación que pueden hacer que el verdadero razonamiento ecuacional sea difícil.

Sin embargo, queda un gran problema. Todavía no tenemos técnicas para probar el teorema libre que necesitamos para el tipo de todo forall b . (a -> b) ⊸ b forall b . (a -> b) ⊸ b . Resulta que las relaciones lógicas actuales (las herramientas que normalmente usamos para hacer tales pruebas) no han sido diseñadas para tomar en cuenta la linealidad de la manera que se necesita. Este problema tiene implicaciones para establecer la corrección para los compiladores que realizan las traducciones de CPS.