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

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?

Primero, seamos explícitos acerca de cómo seqdistingue de λ x . ⊥ :$\bot$$\lambda x . \bot$

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 . $\bot$$\lambda x . \bot$seqseqseq$\lambda$seq$\bot$$\lambda x . \bot$ 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.$\lambda$$[D \to E]$$\bot = \lambda x . \bot$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$\lambda$seq$\bot$$\lambda x . \bot$$\eta$$[D \to E]_\bot$$\bot$$[D \to E]_\bot$$\lambda x . \bot$ , no importa a qué los aplique (sonextensionalmente iguales$\bot$) Pero sí tenemos sequn mapa entre dominios y siempre distingue el fondo de todos los demás elementos.

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

$\lambda x.\, \bot$$\lambda x.\, \bot$ , 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.

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).