haskell - name - meta tags seo
¿Por qué es malo? (2)
Hasta donde sé, una función seq polimórfica es mala porque debilita los teoremas libres o, en otras palabras, algunas igualdades que son válidas sin seq ya no son válidas con seq . Por ejemplo, la igualdad
map g (f xs) = f (map g xs)
contiene todas las funciones g :: tau -> tau'' , todas las listas 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 nuevos elementos.
Para ser honesto, puede inventar elementos, ya que podría "insertar" un error de cómputo / 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]
Para arreglar 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 seq polimórfico, 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 consideramos la lista xs = [False, True] , tenemos
map g (f [False, True]) = map g [True] = [True]
pero en la otra mano
f (map g [False, True]) = f [undefined, True] = [undefined]
Es decir, puede usar seq para hacer que el elemento de una posición determinada de la lista dependa de la definición de otro elemento en la lista. La igualdad se mantiene nuevamente si g es total. Si está interesado en teoremas gratuitos, consulte el generador de teoremas gratuito , que le permite especificar si está considerando un idioma con errores o incluso un idioma con seq . Aunque, esto podría parecer de menor relevancia práctica, seq rompe algunas transformaciones que se utilizan para mejorar el rendimiento de los programas funcionales, por ejemplo, la fusión de foldr / build falla en presencia de seq . Si le interesan más detalles sobre los teoremas libres en presencia de seq , eche un vistazo a los teoremas libres en presencia de seq .
Por lo que yo sé, se sabía que una seq polimórfica rompe ciertas transformaciones cuando se agrega al lenguaje. Sin embargo, las alternativas también tienen desventajas. Si agrega una clase basada en clase de tipo, es posible que tenga que agregar muchas restricciones de clase de tipo a su programa, si agrega un seq algún lugar en el fondo. Además, no había sido una elección omitir seq , ya que se sabía que hay fugas de espacio que se pueden arreglar usando seq .
Finalmente, podría perder algo, pero no veo cómo funcionaría un operador seq de tipo a -> a . La clave de seq es que evalúa una expresión para encabezar la forma normal, si otra expresión se evalúa para encabezar la forma normal. Si seq tiene a -> a tipo a -> a no hay forma de que la evaluación de una expresión dependa de la evaluación de otra expresión.
Haskell tiene una función mágica llamada seq , que toma un argumento de cualquier tipo y lo reduce a la forma normal de la cabeza débil (WHNF).
He leído un par de fuentes [no es que pueda recordar quiénes eran en este momento ...] que afirman que "la seq polimórfica es mala". ¿De qué manera son "malos"?
Del mismo modo, existe la función rnf , que reduce un argumento a la Forma Normal (NF). Pero este es un método de clase; no funciona para tipos arbitrarios. Me parece "obvio" que se podría alterar la especificación del lenguaje para proporcionar esto como una primitiva incorporada, similar a la seq . Esto, presumiblemente, sería "incluso más malo" que simplemente tener seq . ¿De qué manera es esto así?
Finalmente, alguien sugirió que dar seq , rnf , par y similares del mismo tipo que la función id , en lugar de la función const como lo está ahora, sería una mejora. ¿Cómo es eso?
Otro contraejemplo se da en esta respuesta : las mónadas no satisfacen las leyes de mónada con seq y undefined . Y como undefined se puede evitar lo undefined en un lenguaje completo de Turing, el que tiene la culpa es el seq .