ejercicios - ¿Por qué ''cabeza'' de Haskell se cuelga en una lista vacía(o por qué*no*devuelve una lista vacía)?(Filosofía del lenguaje)
ejercicios de listas en haskell (6)
¿Se pierde el polimorfismo al permitir el manejo de listas vacías? Si es así, ¿cómo es eso, y por qué? ¿Hay casos particulares que lo hagan obvio?
El teorema libre para head dice que
f . head = head . $map f
Aplicar este teorema a [] implica que
f (head []) = head (map f []) = head []
Este teorema debe ser válido para cada f , por lo que debe mantenerse para const True y const False . Esto implica
True = const True (head []) = head [] = const False (head []) = False
Por lo tanto, si la head es propiamente polimórfica y la head [] era un valor total, entonces True sería igual a False .
PD. Tengo otros comentarios sobre el trasfondo de su pregunta en el sentido de que si tiene una condición previa de que su lista no está vacía, entonces debe aplicarla usando un tipo de lista no vacía en la firma de su función en lugar de usar una lista.
Nota para otros contribuyentes potenciales: No dude en utilizar notaciones abstractas o matemáticas para expresar su punto. Si encuentro que su respuesta no es clara, le pediré una aclaración, pero de lo contrario, siéntase libre de expresarse de manera cómoda.
Para ser claro: no estoy buscando una head "segura", ni la elección de la head en particular es excepcionalmente significativa. La carne de la pregunta sigue a la discusión de head y head'' , que sirven para proporcionar contexto.
He estado pirateando con Haskell durante algunos meses (hasta el punto de que se ha convertido en mi idioma principal), pero no estoy bien informado sobre algunos de los conceptos más avanzados ni sobre los detalles de la filosofía del lenguaje (aunque Estoy más que dispuesto a aprender). Mi pregunta entonces no es tanto técnica (a menos que sea y simplemente no me doy cuenta) ya que es una de filosofía.
Para este ejemplo, estoy hablando de la head .
Como imagino que sabrás,
Prelude> head []
*** Exception: Prelude.head: empty list
Esto se sigue de head :: [a] -> a . Lo suficientemente justo. Obviamente, uno no puede devolver un elemento de (agitando la mano) ningún tipo. Pero, al mismo tiempo, es simple (si no trivial) definir
head'' :: [a] -> Maybe a
head'' [] = Nothing
head'' (x:xs) = Just x
He visto una pequeña discusión de esto here en la sección de comentarios de ciertas declaraciones. Notablemente, un Alex Stangl dice
''Hay buenas razones para no hacer que todo sea'' seguro ''y lanzar excepciones cuando se violan las condiciones previas''.
No necesariamente cuestiono esta afirmación, pero tengo curiosidad sobre cuáles son estas "buenas razones".
Además, dice Paul Johnson,
''Por ejemplo, podría definir "safeHead :: [a] -> Maybe a", pero ahora, en lugar de manejar una lista vacía o probar que no puede suceder, debe manejar "Nothing" o demostrar que no puede suceder. . ''
El tono que leí de ese comentario sugiere que este es un aumento notable en la dificultad / complejidad / algo, pero no estoy seguro de entender lo que está diciendo.
Un Steven Pruzina dice (en 2011, nada menos),
"Hay una razón más profunda por la que, por ejemplo, ''head'' no puede ser a prueba de choques. Para ser polimórfico pero manejar una lista vacía, ''head'' siempre debe devolver una variable del tipo que está ausente de cualquier lista vacía en particular. Delphic si Haskell pudiera hacer eso ... ".
¿Se pierde el polimorfismo al permitir el manejo de listas vacías? Si es así, ¿cómo es eso, y por qué? ¿Hay casos particulares que lo hagan obvio? Esta sección fue ampliamente respondida por @Russell O''Connor. Cualquier pensamiento adicional es, por supuesto, apreciado.
Voy a editar esto como lo dicta la claridad y la sugerencia. Todos los pensamientos, documentos, etc., que pueda proporcionar serán muy apreciados.
¿Por qué alguien usa head :: [a] -> a lugar de coincidencia de patrones? Una de las razones es porque sabe que el argumento no puede estar vacío y no desea escribir el código para manejar el caso donde el argumento está vacío.
Por supuesto, su head'' de tipo [a] -> Maybe a se define en la biblioteca estándar como Data.Maybe.listToMaybe . Pero si reemplaza un uso de head con listToMaybe , debe escribir el código para manejar el caso vacío, lo que frustra el propósito de usar head .
No estoy diciendo que usar la head sea un buen estilo. Oculta el hecho de que puede dar lugar a una excepción, y en este sentido no es bueno. Pero a veces es conveniente. El punto es que la head sirve para algunos propósitos que no pueden ser atendidos por listToMaybe .
La última cita de la pregunta (sobre polimorfismo) simplemente significa que es imposible definir una función de tipo [a] -> a que devuelva un valor en la lista vacía (como explicó Russell O''Connor en su respuesta ).
Creo que esto es una cuestión de simplicidad y belleza. Lo cual es, por supuesto, en el ojo del espectador.
Si proviene de un fondo Lisp, puede ser consciente de que las listas están compuestas de celdas cons, cada celda tiene un elemento de datos y un puntero a la siguiente celda. La lista vacía no es una lista per se, sino un símbolo especial. Y Haskell va con este razonamiento.
En mi opinión, es más limpio, más simple de razonar y más tradicional, si la lista vacía y la lista son dos cosas diferentes.
... Puedo agregar, si te preocupa que la cabeza no sea segura, no la uses, usa la coincidencia de patrones en su lugar:
sum [] = 0
sum (x:xs) = x + sum xs
Es natural esperar lo siguiente: xs === head xs : tail xs : una lista es idéntica a su primer elemento, seguida del resto. Parece lógico, ¿verdad?
Ahora, vamos a contar el número de conses (aplicaciones de:), sin tener en cuenta los elementos reales, al aplicar la supuesta ''ley'' a [] : [] debería ser idéntica a foo : bar , pero la primera tiene 0 conses, mientras que la última tiene (al menos) uno. Uh oh, algo no está bien aquí!
El sistema de tipos de Haskell, pese a todas sus fortalezas, no puede expresar el hecho de que solo se debe llamar a la head en una lista no vacía (y que la ''ley'' solo es válida para las listas no vacías). El uso de la head transfiere la carga de la prueba al programador, quien debe asegurarse de que no se use en las listas vacías. Creo que los idiomas de tipo dependiente como Agda pueden ayudar aquí.
Finalmente, una descripción un poco más operacional-filosófica: ¿cómo debería ejecutarse head ([] :: [a]) :: a ? Conjurar un valor de tipo a de la nada es imposible (piense en tipos deshabitados tales como data Falsum ), y equivaldría a probar cualquier cosa (a través del isomorfismo de Curry-Howard).
Hay varias formas diferentes de pensar sobre esto. Así que voy a argumentar a favor y en contra de la head'' :
Contra la head'' :
No es necesario tener head'' : dado que las listas son un tipo de datos concreto, todo lo que se puede hacer con head'' se puede hacer mediante la coincidencia de patrones.
Además, con la head'' simplemente intercambias un functor por otro. En algún momento, querrás ponerte al día con las tachuelas de bronce y trabajar un poco en el elemento de la lista subyacente.
En defensa de la head'' :
Pero la coincidencia de patrones oscurece lo que está sucediendo. En Haskell estamos interesados en calcular funciones, lo cual se logra mejor al escribirlas en un estilo sin puntos usando composiciones y combinadores.
Además, al pensar en los funtores [] y Maybe , head'' te permite avanzar y retroceder entre ellos (en particular, la instancia Applicative de [] con pure = replicate ).
Si en su caso de uso una lista vacía no tiene ningún sentido, siempre puede optar por usar NonEmpty en NonEmpty lugar, donde neHead es seguro de usar. Si lo ves desde ese ángulo, no es la función principal la que no es segura, es toda la estructura de datos de la lista (nuevamente, para ese caso de uso).