¿Por qué es malo?

Question

Haskell tiene una función mágica llamada seq, que toma un argumento de cualquier tipo y lo reduce a Forma normal de cabeza débil (WHNF).

He leído un par de fuentes [no es que yo puedo recordar lo que eran ahora ...] que afirman que "polimórfica seq es malo". ¿De qué manera son "malos"?

Del mismo modo, existe la función rnf, que reduce un argumento a Normal Form (NF). Pero este es un método de clase; no funciona para tipos arbitrarios. Me parece "obvio" que se podría modificar la especificación del lenguaje para proporcionar esto como una primitiva incorporada, similar a seq. Esto, presumiblemente, sería "incluso más malo" que simplemente tener seq. ¿De qué manera es esto así?

Finalmente, alguien sugirió que la administración de seq, rnf, par y los similares del mismo tipo que la función id, en lugar de la función const como lo es ahora, sería una mejora. ¿Cómo es eso?

Answer 1

Por lo que yo sé una función polimórfica seq es malo porque debilita teoremas libres o, en otras palabras, algunas igualdades que son válidas sin seq ya no son válidos con seq. Por ejemplo, la igualdad

map g (f xs) = f (map g xs) 

es válido para todas las funciones g :: tau -> tau', todas las listas de xs :: [tau] y todas las funciones polimórficas f :: [a] -> [a]. Básicamente, esta igualdad establece que f solo puede reordenar los elementos de su lista de argumentos o eliminar o duplicar elementos, pero no puede inventar elementos nuevos.

Para ser honesto, puede inventar elementos ya que podría "insertar" un error de computación/tiempo de ejecución sin terminación en las listas, ya que el tipo de error es polimórfico. Es decir, esta igualdad ya se rompe en un lenguaje de programación como Haskell sin seq. Las siguientes definiciones de funciones proporcionan un contraejemplo a la ecuación. Básicamente, en el lado izquierdo g "oculta" el error.

g _ = True 
f _ = [undefined] 

el fin de fijar la ecuación, g tiene que ser estricto, es decir, tiene que asignar un error a un error. En este caso, la igualdad se mantiene nuevamente.

Si agrega un operador polimórfico seq, la ecuación se rompe de nuevo; por ejemplo, la siguiente instanciación es un ejemplo de contador.

g True = True 
f (x:y:_) = [seq x y] 

Si tenemos en cuenta la lista xs = [False, True], tenemos

map g (f [False, True]) = map g [True] = [True] 

pero, por otro lado

f (map g [False, True]) = f [undefined, True] = [undefined] 

Es decir, se puede utilizar seq para hacer que el elemento de una cierta la posición de la lista depende de la definición de otro elemento en la lista. La igualdad se mantiene nuevamente si g es total.Si le interesan los teoremas gratuitos, consulte free theorem generator, que le permite especificar si está considerando un idioma con errores o incluso un idioma con seq. Aunque, esto podría parecer de menor importancia práctica, seq rompe algunas transformaciones que se utilizan para mejorar el rendimiento de los programas funcionales, por ejemplo, foldr/build falla de fusión en presencia de seq. Si le interesan más detalles sobre los teoremas libres en presencia de seq, eche un vistazo al Free Theorems in the Presence of seq.

Por lo que sé, se sabía que una polimórfica seq rompe ciertas transformaciones cuando se agregaba al lenguaje. Sin embargo, las alternativas también tienen desventajas. Si agrega una clase de tipo basada en seq, es posible que tenga que agregar muchas restricciones de clase de tipo a su programa, si agrega un seq en algún lugar en el fondo. Además, no había sido una elección omitir seq porque ya se sabía que hay fugas de espacio que se pueden reparar usando seq.

Finalmente, podría perder algo, pero no veo cómo un operador seq del tipo a -> a funcionaría. La clave de seq es que evalúa una expresión para encabezar la forma normal, si se evalúa otra expresión para encabezar la forma normal. Si seq tiene el tipo a -> a, no hay forma de que la evaluación de una expresión dependa de la evaluación de otra expresión.

Answer 2

Otro contraejemplo se da en this answer - las mónadas no satisfacen las leyes de mónada con seq y undefined. Y dado que undefined no se puede evitar en un lenguaje Turing-completo, el único culpable es seq.