¿Cuál es el razonamiento detrás de hacer que el no determinismo sea una característica de Haskell?

Sabemos que en Prolog , los predicados no deterministas son una característica utilizada para reducir los problemas combinatorios .

En Haskell vemos un comportamiento no determinista similar al de Prolog en la Lista Mónada .

En Haskell también vemos el no determinismo al elegir el orden de evaluación thunk :

Pero no hay nada que le diga a GHC cuál de esos thunks debe evaluarse primero, y por lo tanto, GHC tiene plena libertad para elegir el thunk que se evalúe primero.

Esto es fascinante, y algo liberador. Me pregunto (aparte de lidiar con problemas lógicos como las ocho reinas ) a qué principio sirve. ¿Hubo alguna gran idea o gran problema que intentaban resolver con el no determinismo?

Mi pregunta es: ¿Cuál es el razonamiento detrás de hacer que el no determinismo sea una característica de Haskell?

Si bien es cierto que ambos aspectos citados en las preguntas aparecen como formas de no determinismo, de hecho son bastante diferentes tanto en cómo funcionan como en sus objetivos. Por lo tanto, cualquier respuesta tiene que dividirse necesariamente en dos partes.

Orden de evaluación

Haskell no exige ninguna orden de ejecución particular en la evaluación de thunks esencialmente debido a dos razones.

1. En primer lugar, Haskell es un lenguaje puramente funcional, por lo que tiene garantizada una transparencia referencial (si no juega con unsafePerformIO& co). Esto significa que la evaluación de cualquier expresión, por ejemplo , f xdará como resultado el mismo resultado sin importar cuántas veces se evalúe y sin importar en qué parte del programa se evalúe (suponiendo fy xvinculando los mismos valores en los ámbitos considerados, de curso). Por lo tanto, ordenar cualquier orden particular de ejecución no tendría ningún propósito , porque cambiarlo no produciría ningún efecto observable en el resultado del programa. En este sentido, esto no es realmente una forma de no determinismo, al menos no es una forma observable uno, ya que las diferentes ejecuciones posibles del programa son semánticamente equivalentes.

Sin embargo, cambiar el orden de ejecución puede tener un efecto en el rendimiento del programa, y ​​dejar al compilador la libertad de manipular el orden a su voluntad es fundamental para lograr el rendimiento sorprendente que un compilador como GHC puede obtener compilando un nivel tan alto. lenguaje de nivel Como ejemplo, piense en una transformación clásica de fusión de flujo:

map f . map g = map (f.g)

Esta igualdad simplemente significa que aplicar dos funciones a una lista maptiene el mismo resultado que aplicar una vez la composición de las dos funciones. Esto solo es cierto debido a la transparencia referencial, y es un tipo de transformación que el compilador siempre puedeaplicar, pase lo que pase. Si cambiar el orden de ejecución de las tres funciones tuviera efectos en el resultado de la expresión, esto no sería posible. Por otro lado, compilarlo en la segunda forma en lugar de la primera puede tener un gran impacto en el rendimiento, ya que evita la construcción de una lista temporal y solo atraviesa la lista una vez. El hecho de que GHC pueda aplicar automáticamente dicha transformación es una consecuencia directa de la transparencia referencial y el orden no fijo de ejecución y es uno de los aspectos clave del gran desempeño que Haskell puede lograr.

2. Haskell es un lenguaje vago . Esto significa que no es necesario evaluar ninguna expresión en particular a menos que su resultado sea realmente necesario, y esto también podría ser nunca. La pereza es una característica a veces debatida y algunos otros lenguajes funcionales lo evitan o lo limitan para ser aceptado, pero en el contexto de Haskell es una característica clave en la forma en que se usa y diseña el lenguaje. La pereza es otra herramienta poderosa en manos del optimizador del compilador, y lo más importante, permite que el código se componga fácilmente.

Para ver a qué me refiero con facilidad de composición, considere un ejemplo cuando tiene una función producer :: Int -> [Int]que realiza una tarea compleja para calcular una lista de algún tipo de datos a partir de un argumento de entrada, y consumer :: [Int] -> Intque es otra función compleja que computa un resultado de una lista de datos de entrada. Los ha escrito por separado, los ha probado, los ha optimizado con mucho cuidado y los ha utilizado de forma aislada en diferentes proyectos. Ahora en el próximo proyecto sucede que tienes que recurrir consumeral resultado deproducer. En un lenguaje no perezoso, esto puede no ser óptimo, ya que puede darse el caso de que la tarea combinada se implemente más eficientemente sin construir una estructura de lista temporal. Para obtener una implementación optimizada, tendría que volver a implementar la tarea combinada desde cero, volver a probarla y volver a optimizarla.

En Haskell esto no es necesario, y llamar a la composición de las dos funciones consumer . producerestá perfectamente bien. La razón es que no se requiere que el programa produzca realmente el resultado completo producerantes de entregarlo consumer. De hecho, tan pronto como consumernecesite el primer elemento de su lista de entrada, el código correspondiente producerse ejecutará tanto como sea necesario para producirlo, y no más. Cuando se necesita el segundo elemento, se computará. Si algún elemento no será necesario consumer, no se calculará en absoluto, ahorrando efectivamente cálculos inútiles. La ejecución de consumeryproducerefectivamente se intercalará, no solo evitando el uso de la memoria de la estructura de la lista intermedia, sino también evitando cálculos inútiles, y la ejecución probablemente sería similar a la versión combinada escrita a mano que de lo contrario tendría que escribir usted mismo. Esto es lo que quise decir con composición . Usted tenía dos piezas de código bien probadas y con buen rendimiento y podía componerlas obteniendo de forma gratuita una pieza de código bien probada y con buen rendimiento.

Mónadas no deterministas

El uso del comportamiento no determinista provisto por la Lista de mónadas y similares es totalmente diferente. Aquí no se trata de proporcionar al compilador los medios para optimizar su programa, sino de expresar de manera clara y concisa los cálculos que son inherentemente no deterministas.

La interfaz de la Data.Boolean.SatSolverbiblioteca proporciona un ejemplo de lo que quiero decir . Proporciona un solucionador DPLL SAT muy simple implementado en Haskell. Como ya sabrás, resolver el problema SAT implica encontrar una asignación de variables booleanas que satisfaga una fórmula booleana. Sin embargo, puede haber más de una de esas tareas, y uno puede necesitar encontrar alguna de ellas, o iterar sobre todas ellas, dependiendo de la aplicación. Por lo tanto, muchas bibliotecas tendrán dos funciones diferentes como getSolutiony getAllSolutions. En cambio, esta biblioteca solo tiene una función solve, con el siguiente tipo:

solve :: MonadPlus m => SatSolver -> m SatSolver

Aquí, el resultado es un SatSolvervalor envuelto dentro de una mónada de tipo no especificado, que sin embargo está obligado a implementar la MonadPlusclase de tipo. Esta clase de tipo es la que representa el tipo de no determinismo proporcionado por la mónada de la lista, y de hecho las listas son instancias. Todas las funciones que operan en SatSolvervalores devuelven sus resultados en una MonadPlusinstancia. Entonces, suponga que tiene la fórmula p || !qy desea resolverla restringiendo los resultados que establecen qverdadero, entonces el uso es el siguiente (las variables se numeran en lugar de identificarse por nombre):

expr = Var 1 :||: Not (Var 2)

task :: MonadPlus m => m SatSolver
task = do
  pure newSatSolver
  assertTrue expr
  assertTrue (Var 2)

Observe cómo la instancia de mónada y la notación do ocultan todos los detalles de bajo nivel de cómo las funciones manejan la SatSolverestructura de datos, y nos permiten expresar claramente nuestra intención.

Ahora, si desea obtener todos los resultados, simplemente use solveen un contexto donde su resultado tiene que ser una lista. Lo siguiente imprimirá todos los resultados en pantalla (suponiendo una Showinstancia para SatSolver, que no existe, pero perdóname este punto).

main = sequence . map print . solve task

Sin embargo, las listas no son las únicas instancias de MonadPlus. MaybeEs otra instancia. Entonces, si solo necesita una solución, sin importar cuál, puede usar solvecomo si devolviera un Maybe SatSolvervalor:

main = case solve task of 
  Nothing -> putStrLn "No solution"
  Just result -> print result

Ahora supongamos que tiene dos tareas por lo construyeron, tasky task2, y desea obtener una solución a cualquiera de ellos. Una vez más, todo se une para permitirnos componer nuestros bloques de construcción preexistentes:

combinedTask = task <|> task2

donde <|>es una operación binaria proporcionada por la Alternativeclase de tipos, que es una superclase de MonadPlus. Esto nuevamente nos permite expresar claramente nuestra intención, reutilizando el código sin cambios. El no determinismo se expresa claramente en código, no se oculta bajo los detalles de cómo se implementa realmente el no determinismo. Le sugiero que eche un vistazo a los combinadores integrados en la parte superior de la Alternativeclase de tipos para obtener más ejemplos.

Las mónadas no deterministas, como las listas, no son solo una forma de expresar buenos ejercicios, sino que ofrecen una forma de diseñar un código elegante y reutilizable que exprese claramente la intención en la implementación de tareas que son inherentemente no deterministas.