¿Es la equivalencia eta para funciones compatible con la operación seq de Haskell?

14

Lema: Suponiendo equivalencia eta tenemos eso (\x -> ⊥) = ⊥ :: A -> B.

Prueba: ⊥ = (\x -> ⊥ x)por equivalencia eta y (\x -> ⊥ x) = (\x -> ⊥)por reducción bajo la lambda.

El informe Haskell 2010, sección 6.2 especifica la seqfunción mediante dos ecuaciones:

seq :: a -> b -> b
seq ⊥ b = ⊥
seq ab = b, si a ≠ ⊥

Luego afirma "Como consecuencia, ⊥ no es lo mismo que \ x -> ⊥, ya que seq puede usarse para distinguirlos".

Mi pregunta es, ¿es realmente una consecuencia de la definición de seq?

El argumento implícito parece ser que seqsería indiscutible si seq (\x -> ⊥) b = ⊥. Sin embargo, no he podido demostrar que tal seqsería indiscutible. Me parece que seqes monótono y continuo, lo que lo pone en el ámbito de ser computable.

Un algoritmo que se implemente, como seq, podría funcionar al intentar buscar algún xlugar f x ≠ ⊥enumerando el dominio que fcomienza con ⊥. Aunque tal implementación, incluso si es posible, se vuelve bastante complicada una vez que queremos hacer seqpolimórficos.

¿Hay alguna prueba de que no hay computable seqque se identifica (\x -> ⊥)con el ⊥ :: A -> B? Alternativamente, ¿hay algo de construcción del seqque se identifica (\x -> ⊥)con el ⊥ :: A -> B?

Russell O'Connor
fuente

Respuestas:

6

Primero, seamos explícitos acerca de cómo seqdistingue de λ x . :λx.

bottom :: a
bottom = bottom

eta :: a -> b
eta x = bottom

-- This terminates
fortytwo = seq eta 42

-- This does not terminate
infinity = seq bottom 42

Por lo tanto, es un hecho experimental que en Haskell y λ x . son operacionalmente distinguibles. También es un hecho, y bastante obvio, que es computable porque Haskell lo calcula. Mucho sobre Haskell. Usted está preguntando sobre la redacción muy particular de la documentación de Haskell. Lo leo como diciendo que se supone que satisface las dos ecuaciones dadas, pero esas dos ecuaciones no son suficientes para la definición de . He aquí por qué: puedo darle dos modelos de cálculo λ (simplemente tipado) en el que es computable y satisface las ecuaciones dadas, pero en uno de los modelos y λ x . λx.seqseqseqλseqλx. de acuerdo, mientras que en el otro no.

En un modelo teórico de dominio simple donde las expresiones se interpretan en el dominio de funciones continuas [ D E ] tenemos = λ x . Obviously , obviamente. Tome dominios Scott efectivos o algo así para que todo sea computable. Es fácil de definir en tal modelo.λ[DE]=λx.seq

También podemos tener un modelo de cálculo en el que se distingue y λ x . , y luego, por supuesto, η -rule no puede sostenerse. Por ejemplo, podemos hacer esto interpretando funciones en el dominio [ D E ] , es decir, el dominio del espacio de funciones con un fondo adicional adjunto. Ahora es, bueno, la parte inferior de [ D E ] , mientras que λ x . es el elemento justo encima de él. No se pueden distinguir por aplicación porque ambos evalúanλseqλx.η[DE][DE]λx. , no importa a qué los aplique (sonextensionalmente iguales) Pero sí tenemos sequn mapa entre dominios y siempre distingue el fondo de todos los demás elementos.

Andrej Bauer
fuente
1
Es un hecho experimental que en GHC y / o Abrazos ⊥ y λx.⊥. Afortunadamente, Haskell no se define por una implementación. Mi pregunta sugiere que Haskell está subespecificado con respecto a seq.
Russell O'Connor
¿Puede dar una referencia a lo que quiere decir con "dominios de Scott efectivos" Presumiblemente, eso no implica que el orden parcial sea decidible. Además, el STLC no es polimórfico, pero Haskell sí. Por lo general, Haskell se interpreta en el Sistema F o en uno de sus derivados. ¿Cómo afecta esto a tu argumento?
Russell O'Connor
Sección 1.1.4 de mi Ph.D. disertación andrej.com/thesis/thesis.pdf tiene una breve definición de dominios Scott efectivos, y este es en realidad el primer éxito de Google que está disponible gratuitamente.
Andrej Bauer
2
Si escribe una prueba para mí, obtendrá una implementación de Haskell 98 donde la regla eta se mantiene permitiendo que (foldr (\ ab -> fab) z xs) se optimice a (foldr fz xs) causando un aumento de rendimiento asintótico de O (n ^ 2) a O (n) (ver ghc.haskell.org/trac/ghc/ticket/7436 ). Más convincente permitirá que un NewTypeWrapper en (NewTypeWrapper. F) se optimice sin forzar que f se expanda y evitará algunas penalizaciones de rendimiento asintótico impuestas actualmente por newTypes en GHC (en el uso de foldr, por ejemplo).
Russell O'Connor
1
En realidad, deberías asegurarte de que tu compilador siempre implemente como . Es decir, podría tener la tentación de no siempre contraerse y, en principio, λ x . y serían "a veces distinguibles", una situación muy peligrosa. Para asegurarse de que este no sea el caso, debe implementar de manera inteligente, lo que implica generar infinitos procesos, cada uno aplicando su función a un elemento básico. Si alguno de los procesos termina, entonces puede continuar. Sería interesante ver si podemos hacer esto secuencialmente. Hmm λx.λx.seqseq
Andrej Bauer
2

Tenga en cuenta que la especificación para la seqque cita no es su definición. Para citar el informe Haskell "La función seq está definida por las ecuaciones : [y luego las ecuaciones que usted da]".

El argumento sugerido parece ser que seq sería incuestionable si seq (\ x -> ⊥) b = ⊥.

Tal comportamiento violaría la especificación de seq .

Es importante destacar que, dado que seqes polimórfico, seqno se puede definir en términos de deconstructores (proyecciones / coincidencia de patrones, etc.) en ninguno de los dos parámetros.

¿Hay alguna prueba de que no hay una secuencia computable que identifique (\ x -> ⊥) con ⊥ :: A -> B?

Si seq' (\x -> ⊥) b, uno podría pensar que podríamos aplicar el primer parámetro (que es una función) a algún valor y luego sacar ⊥. Pero, seqnunca puede identificar el primer parámetro con un valor de función (incluso si resulta ser uno para algún uso seq) debido a su tipo polimórfico paramétrico. La parametricidad significa que no sabemos nada sobre los parámetros. Además, seqnunca puede tomar una expresión y decidir "¿es esto ⊥?" (cf. el problema de detención), seqsolo puede intentar evaluarlo y divergir a ⊥.

Lo que seqhace es evaluar el primer parámetro (no completamente, sino en "forma normal de cabeza débil" [1], es decir, en el constructor superior), luego devolver el segundo parámetro. Si el primer parámetro resulta ser (es decir, un cálculo que no termina), entonces evaluarlo hace seqque no termine, y así seq ⊥ a = ⊥.

[1] Teoremas libres en presencia de seq - Johann, Voigtlander http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf

dorchard
fuente
La especificación que doy para seq es la definición de seq porque eso es exactamente lo que dice el informe Haskell 2010 en la Sección 6.2. El informe Haskell 2010 no admite su definición de operación de seq: las palabras "forma normal de la cabeza" solo aparecen una vez en el informe en un contexto totalmente diferente. También es inconsistente con mi comprensión de que GHC a menudo reducirá el segundo argumento a seq antes del primer argumento, o el primer argumento no se reducirá en absoluto porque el analizador de rigurosidad ha demostrado que no es estáticamente inferior.
Russell O'Connor
La parametricidad no dice directamente que no podemos aplicar ningún deconstructor, ni dice que nunca podemos identificar el primer parámetro con un valor de función. Todo lo que dice la parámetroidad para el cálculo lambda polimórfico con puntos de fijación es que seq puede absorber funciones estrictas, o más generalmente ciertas relaciones estrictas para términos contienen seq. Admito que es plausible que la parametricidad se pueda usar para probar (\ x -> ⊥) & ne; ⊥, pero me gustaría ver una prueba rigurosa.
Russell O'Connor
En el caso de una función f : forall a . a -> T(donde Tes algún otro tipo), entonces fno puede aplicar ningún deconstructor a su primer argumento, ya que no sabe qué deconstructores aplicar. No podemos hacer un "caso" sobre los tipos. He tratado de mejorar la respuesta anterior (incluida la información sobre la seqevaluación de la forma normal de la cabeza).
dorchard
Puedo intentar hacer la prueba rigurosa más adelante si encuentro tiempo (usar relaciones al estilo de Reynolds podría ser un buen enfoque).
dorchard
@ RussellO'Connor: la descripción de seq no es "inconsistente" con esos comportamientos, es solo una especificación operativa (y los comportamientos son optimizaciones que no cambian el resultado final).
Blaisorblade
2

λx.λx. , la evaluación termina. El comentario "Como consecuencia ..." en el informe Haskell supone que el lector lo sabe.

Samson Abramsky consideró este tema hace mucho tiempo y escribió un artículo llamado " El cálculo perezoso de Lambda ". Entonces, si quieres definiciones formales, aquí es donde puedes mirar.

Uday Reddy
fuente
1
Aparentemente, estos detalles solo se definen al desugarse en el "núcleo Haskell". ¿Dónde se define es? El informe dice, en la Sec. 1.2 : "Aunque el núcleo no se especifica formalmente, es esencialmente una variante ligeramente azucarada del cálculo lambda con una semántica denotacional directa. La traducción de cada estructura sintáctica en el núcleo se da a medida que se introduce la sintaxis".
Blaisorblade
El informe Haskell 2010 dice lo mismo , sorprendentemente.
Blaisorblade
Gracias por la referencia a Abramsky! Lo hojeé para ver cómo responde la pregunta y se me ocurrió la siguiente respuesta: cstheory.stackexchange.com/a/21732/989
Blaisorblade
2

Demostrando que λ x. Ω ‌ ≠ Ω es uno de los objetivos que Abramsky establece para su teoría del cálculo perezoso lambda (página 2 de su artículo , ya citado por Uday Reddy), porque ambos están en forma normal de cabeza débil. A partir de la definición 2.7, discute explícitamente que eta-reducción λ x. M x → M no es generalmente válido, pero es posible si M termina en todos los entornos. Esto no significa que M debe ser una función total, solo que la evaluación de M debe terminar (reduciéndose a una lambda, por ejemplo).

Su pregunta parece estar motivada por preocupaciones prácticas (rendimiento). Sin embargo, aunque el Informe Haskell podría ser menos que completamente claro, dudo que iguale λ x. ⊥ ‌with ⊥ produciría una implementación útil de Haskell; si implementa Haskell '98 o no es discutible, pero dado el comentario, está claro que los autores pretendieron que fuera así.

Finalmente, ¿cómo seq para generar elementos para un tipo de entrada arbitraria? (Sé que QuickCheck define la clase de tipo Arbitraria para eso, pero no está permitido agregar tales restricciones aquí). Esto viola la parametricidad.

Actualizado : no logré codificar esto correctamente (porque no soy tan fluido en Haskel), y arreglar esto parece requerir runSTregiones anidadas . Intenté usar una sola celda de referencia (en la mónada ST) para guardar tales elementos arbitrarios, leerlos más tarde y hacerlos disponibles universalmente. La parametricidad demuestra que a break_parametricitycontinuación no se puede definir (excepto al regresar al fondo, por ejemplo, un error), mientras que podría recuperar los elementos que generaría la secuencia propuesta.

import Control.Monad.ST
import Data.STRef
import Data.Maybe

produce_maybe_a :: Maybe a
produce_maybe_a = runST $ do { cell <- newSTRef Nothing; (\x -> writeSTRef cell (Just x) >> return x) `seq` (readSTRef cell) }

break_parametricity :: a
break_parametricity = fromJust produce_maybe_a

Tengo que admitir que estoy un poco confuso en formalizar la prueba de parametricidad necesaria aquí, pero este uso informal de la parametricidad es estándar en Haskell; pero aprendí de los escritos de Derek Dreyer que la teoría necesaria se está resolviendo rápidamente en estos últimos años.

EDICIONES:

  • Ni siquiera estoy seguro de si necesita esas extensiones, que se estudian para lenguajes ML, imperativos y sin tipo, o si las teorías clásicas de parametricidad cubren Haskell.
  • Además, mencioné a Derek Dreyer simplemente porque más tarde me encontré con el trabajo de Uday Reddy, lo aprendí recientemente de "La esencia de Reynolds". (Solo comencé a leer realmente literatura sobre parametricidad en el último mes más o menos).
Blaisorblade
fuente
La evaluación (\x -> writeSTRef cell (Just x) >> return x)en entradas aleatorias no ejecuta una escritura en la celda. Solo runSTse ejecutan los comandos ST que entran en la secuencia que se pasa . Del mismo modo, la ejecución main = (putStrLn "Hello") `seq` (return ())no imprime nada en la pantalla.
Russell O'Connor
@ RussellO'Connor, por supuesto que tiene razón: las pruebas son difíciles ya que seq no tiene el comportamiento que discutimos. Pero sigo pensando que generar elementos rompe la parametricidad per se. Intentaré arreglar la respuesta para ejemplificar eso.
Blaisorblade
Hm, la solución obvia a la respuesta requiere anidar las regiones runST y usar la celda de la región externa en la interna, pero eso no está permitido.
Blaisorblade