haskell functional-programming ml

haskell - ¿Pueden los compiladores deducir/probar matemáticamente?



functional-programming ml (6)

La respuesta

No, los compiladores no hacen ese tipo de cosas.

Una razón por la cual

Y para sus ejemplos, incluso sería incorrecto: como no dio anotaciones de tipo, el compilador de Haskell deducirá el tipo más general, que sería

foldr (+) 0 [ 1 ..10] :: Num a => a

y similar

(/list -> sum (reverse list)) :: Num a => [a] -> a

y la instancia de Num para el tipo que se está utilizando podría no cumplir con las leyes matemáticas requeridas para la transformación que usted sugiere. El compilador debe, antes que nada, evitar cambiar el significado (es decir, la semántica) de su programa.

Más pragmáticamente: los casos en que el compilador podría detectar tales transformaciones a gran escala rara vez ocurren en la práctica, por lo que no valdría la pena implementarlas.

Una excepción

Las notables excepciones son las transformaciones lineales en los bucles. La mayoría de los compiladores reescribirán

for (int i = 0; i < n; i++) { ... 200 + 4 * i ... }

a

for (int i = 0, j = 200; i < n; i++, j += 4) { ... j ... }

o algo similar, ya que ese patrón ocurre a menudo en el código que trabaja en una matriz.

Estoy empezando a aprender un lenguaje de programación funcional como Haskell , ML y la mayoría de los ejercicios mostrarán cosas como:

foldr (+) 0 [ 1 ..10]

que es equivalente a

sum = 0 for( i in [1..10] ) sum += i

Así que eso me lleva a pensar ¿por qué el compilador no puede saber que esto es Progresión Aritmética y usar la fórmula O (1) para calcular? ¿Especialmente para lenguajes FP puros sin efectos secundarios? Lo mismo se aplica para

sum reverse list == sum list

Dados a + b = b + a y la definición de inverso, ¿pueden los compiladores / idiomas probarlo automáticamente?

Como han dicho otros, no está claro que sus simplificaciones se mantengan en Haskell. Por ejemplo, puedo definir

newtype NInt = N Int instance Num NInt where N a + _ = N a N b * _ = N b ... -- etc

y ahora sum . reverse :: Num [a] -> a sum . reverse :: Num [a] -> a no es igual a sum :: Num [a] -> a ya que puedo especializar cada uno a [NInt] -> NInt where sum . reverse == sum sum . reverse == sum claramente no se mantiene.

Esta es una tensión general que existe en torno a la optimización de las operaciones "complejas": en realidad, se necesita mucha información para probar con éxito que está bien optimizar algo. Esta es la razón por la que la optimización del compilador de sintaxis que existe es generalmente monomórfica y está relacionada con la estructura de los programas. Por lo general, es un dominio tan simplificado que "no hay forma" de que la optimización salga mal. Incluso eso a menudo es inseguro porque el dominio nunca es tan simplificado y conocido por el compilador.

Como ejemplo, una optimización sintáctica de "alto nivel" muy popular es la fusión de flujos. En este caso, al compilador se le da suficiente información para saber que la fusión de flujos puede ocurrir y es básicamente seguro, pero incluso en este ejemplo canónico tenemos que esquivar las nociones de no terminación.

Entonces, ¿qué se necesita para que /x -> sum [0..x] sea ​​reemplazado por /x -> x*(x + 1)/2 ? El compilador necesitaría una teoría de números y álgebra incorporada. Esto no es posible en Haskell o ML, pero se hace posible en idiomas escritos de manera dependiente como Coq, Agda o Idris. Allí podrías especificar cosas como

revCommute :: (_+_ :: a -> a -> a) -> Commutative _+_ -> foldr _+_ z (reverse as) == foldr _+_ z as

y luego, teóricamente, diga al compilador que revCommute a escribir de acuerdo con revCommute . Esto aún sería difícil y delicado, pero al menos tendríamos suficiente información. Para ser claros, estoy escribiendo algo muy extraño arriba, un tipo dependiente. El tipo no solo depende de la capacidad de introducir tanto un tipo como un nombre para el argumento en línea, sino también la existencia de la sintaxis completa de su idioma "en el nivel de tipo".

Sin embargo, hay muchas diferencias entre lo que acabo de escribir y lo que harías en Haskell. Primero, para formar una base donde tales promesas puedan tomarse en serio, debemos deshacernos de la recursión general (y, por lo tanto, ya no tenemos que preocuparnos por cuestiones de no terminación como lo hace la fusión de corrientes). También debemos tener suficiente estructura para crear algo como la promesa Commutative _+_ --- esto probablemente depende de que exista una teoría completa de operadores y matemáticas incorporada en la biblioteca estándar del idioma, de lo contrario, necesitaría crearla usted mismo. Finalmente, la riqueza del sistema de tipos requerido para expresar incluso este tipo de teorías agrega mucha complejidad a todo el sistema y elimina la inferencia de tipos tal como la conocemos hoy.

Pero, dada toda esa estructura, nunca podría crear una obligación Commutative _+_ para el _+_ definido para trabajar en NInt s, por lo que podemos estar seguros de que foldr (+) 0 . reverse == foldr (+) 0 foldr (+) 0 . reverse == foldr (+) 0 realidad se mantiene.

Pero ahora tendríamos que decirle al compilador cómo realizar esa optimización. Para stream-fusion, las reglas del compilador solo se activan cuando escribimos algo exactamente en la forma sintáctica correcta para que sea "claramente" una redex de optimización. Los mismos tipos de restricciones se aplicarían a nuestra sum . reverse Regla sum . reverse . De hecho, ya estamos hundidos porque.

foldr (+) 0 . reverse foldr (+) 0 (reverse as)

no coinciden Son "obviamente" lo mismo debido a algunas reglas que podríamos probar sobre (.) , Pero eso significa que ahora el compilador debe invocar dos reglas incorporadas para poder realizar nuestra optimización.

Al final del día, necesita una búsqueda de optimización muy inteligente sobre los conjuntos de leyes conocidas para lograr los tipos de optimizaciones automáticas de las que habla.

Así que no solo agregamos mucha complejidad a todo el sistema, requerimos mucho trabajo de base para incorporar algunas teorías algebraicas útiles, y perdemos la integridad de Turing (lo que podría no ser lo peor), también obtenemos una gran dificultad. Prometemos que nuestra regla se disparará incluso a menos que realicemos una búsqueda dolorosa durante la compilación.

Blech

El compromiso que existe hoy en día tiende a ser que a veces tenemos suficiente control sobre lo que se está escribiendo para estar seguros de que se puede realizar una cierta optimización obvia . Este es el régimen de la fusión de flujos y requiere muchos tipos ocultos, pruebas escritas cuidadosamente, explotaciones de parametricidad y agitar las manos antes de que sea algo en lo que la comunidad confía lo suficiente como para ejecutarse en su código.

Y ni siquiera siempre se dispara. Para ver un ejemplo de la lucha contra ese problema, eche un vistazo a la fuente de Vector para todos los pragmas de REGLAS que especifican todas las circunstancias comunes donde deberían activarse las optimizaciones de la fusión de flujos de Vector .

Todo esto no es en absoluto una crítica de las optimizaciones del compilador o las teorías de tipos dependientes. Ambos son realmente increíbles. En cambio, es solo una amplificación de las compensaciones involucradas en la introducción de tal optimización. No debe hacerse a la ligera.

Dato curioso: dadas dos fórmulas arbitrarias, ¿ambas dan la misma salida para las mismas entradas? ¡La respuesta a esta pregunta trivial no es computable! En otras palabras, es matemáticamente imposible escribir un programa de computadora que siempre dé la respuesta correcta en tiempo finito.

Dado este hecho, tal vez no sea sorprendente que nadie tenga un compilador que pueda transformar mágicamente cada computación posible en su forma más eficiente.

Además, ¿no es este el trabajo del programador? Si desea que la suma de una secuencia aritmética sea lo suficientemente común para que sea un cuello de botella en el rendimiento, ¿por qué no escribir un código más eficiente? De manera similar, si realmente quiere los números de Fibonacci (¿por qué?), Use el algoritmo O (1).

Las optimizaciones que tenga en mente probablemente no se realizarán incluso en presencia de tipos monomórficos, porque hay muchas posibilidades y tanto conocimiento requerido. Por ejemplo, en este ejemplo:

sum list == sum (reverse list)

El compilador necesitaría saber o tener en cuenta los siguientes hechos:

  • suma = foldl (+) 0
  • (+) es conmutativo
  • lista inversa es una permutación de lista
  • foldl xcl, donde x es conmutativo y c es una constante, produce el mismo resultado para todas las permutaciones de l.

Todo esto parece trivial. Claro, lo más probable es que el compilador busque la definición de sum y la incluya. Se podría requerir que (+) sea conmutativo, pero recuerde que + es simplemente otro símbolo sin un significado adjunto para el compilador. El tercer punto requeriría que el compilador demuestre algunas propiedades no triviales sobre el reverse .

Pero el punto es:

  1. No desea realizar el compilador para hacer esos cálculos con todas y cada una de las expresiones. Recuerde, para que esto sea realmente útil, tendría que acumular mucho conocimiento sobre muchas, muchas funciones estándar y operadores.

  2. Aún no puede reemplazar la expresión anterior con True menos que pueda descartar la posibilidad de que la lista o algún elemento de la lista esté en la parte inferior. Por lo general, uno no puede hacer esto. Ni siquiera se puede hacer la siguiente optimización "trivial" de fx == fx en todos los casos

    f x `seq` True

Para, considere

f x = (undefined :: Bool, x)

entonces

f x `seq` True ==> True f x == f x ==> undefined

Dicho esto, con respecto a su primer ejemplo ligeramente modificado para el monomorfismo:

f n = n * foldl (+) 0 [1..10] :: Int

es imaginable optimizar el programa moviendo la expresión fuera de su contexto y reemplazándola con el nombre de una constante, como así:

const1 = foldl (+) 0 [1..10] :: Int f n = n * const1

Esto se debe a que el compilador puede ver que la expresión debe ser constante.

Lo que estás describiendo parece una super-compilation . En su caso, si la expresión tuviera un tipo monomorphic como Int (a diferencia del número polimórfico Num a => a ), el compilador podría inferir que la expresión foldr (+) 0 [1 ..10] no tiene dependencias externas, por lo tanto Podría ser evaluado en tiempo de compilación y reemplazado por 55 . Sin embargo, AFAIK ningún compilador convencional actualmente realiza este tipo de optimización.

(En la programación funcional, la "prueba" generalmente se asocia con algo diferente. En los idiomas con tipos dependientes, los tipos son lo suficientemente poderosos para expresar una proposición compleja y luego a través de los programas de correspondencia Curry-Howard se convierten en pruebas de tales proposiciones).

Los compiladores generalmente no intentan probar este tipo de cosas automáticamente, porque es difícil de implementar.

Además de agregar la lógica al compilador para transformar un fragmento de código en otro, debe tener mucho cuidado de que solo intente hacerlo cuando sea realmente seguro, es decir, a menudo hay muchas "condiciones secundarias" de las que preocuparse. Por ejemplo, en su ejemplo anterior, alguien podría haber escrito una instancia de la clase de tipo Num (y, por tanto, el operador (+) ) donde a + b no es b + a .

Sin embargo, GHC tiene reglas de reescritura que puede agregar a su propio código fuente y podría usarse para cubrir algunos casos relativamente simples como los que enumera anteriormente, particularmente si no está demasiado preocupado por las condiciones secundarias.

Por ejemplo, y no he probado esto, puede usar la siguiente regla para uno de sus ejemplos anteriores:

{-# RULES "sum/reverse" forall list . sum (reverse list) = sum list #-}

Tenga en cuenta los paréntesis alrededor de reverse list : lo que ha escrito en su pregunta en realidad significa (sum reverse) list y no verificará la tipografía.

EDITAR:

Mientras busca fuentes oficiales y sugerencias para investigar, he enumerado algunas. Obviamente, es difícil demostrar que es negativo, pero el hecho de que nadie haya dado un ejemplo de un compilador de propósito general que haga este tipo de cosas de forma rutinaria es probablemente una evidencia bastante sólida en sí misma.

  • Como han señalado otros, incluso las optimizaciones aritméticas simples son sorprendentemente peligrosas, particularmente en los números de punto flotante, y los compiladores generalmente tienen banderas para apagarlos, por ejemplo, Visual C ++ , gcc . Incluso la aritmética de enteros no siempre es clara y las personas ocasionalmente tienen grandes argumentos sobre cómo lidiar con cosas como el desbordamiento.

  • Como señaló Joachim, las variables de enteros en los bucles son un lugar donde se aplican optimizaciones ligeramente más sofisticadas porque en realidad hay ganancias significativas que se pueden obtener. El libro de Muchnick es probablemente la mejor fuente general sobre el tema, pero no es tan barato. La página de wikipedia sobre reducción de la fuerza es probablemente una introducción tan buena como cualquiera de las optimizaciones estándar de este tipo, y tiene algunas referencias a la literatura relevante.

  • FFTW es un ejemplo de una biblioteca que realiza internamente todo tipo de optimización matemática. Parte de su código es generado por un compilador personalizado que los autores escribieron específicamente para este propósito. Vale la pena porque los autores tienen conocimientos de optimizaciones de dominio específico que, en el contexto específico de la biblioteca, merecen el esfuerzo y son seguros.

  • La gente a veces usa la metaprogramación de plantillas para escribir "bibliotecas de optimización automática" que, de nuevo, podrían depender de las identidades aritméticas, vea, por ejemplo, Blitz++ . La tesis doctoral de Todd Veldhuizen tiene una buena visión general.

  • Si desciendes en los reinos del juguete y los compiladores académicos, todo tipo de cosas irá. Por ejemplo, mi propia tesis de doctorado trata sobre la escritura de programas funcionales ineficientes junto con pequeños scripts que explican cómo optimizarlos. Muchos de los ejemplos (ver Capítulo 6) se basan en la aplicación de reglas aritméticas para justificar las optimizaciones subyacentes.

Además, vale la pena enfatizar que los últimos ejemplos son optimizaciones especializadas que se aplican solo a ciertas partes del código (por ejemplo, llamadas a bibliotecas específicas) donde se espera que valga la pena. Como han señalado otras respuestas, es simplemente demasiado costoso para un compilador buscar todos los lugares posibles en un programa completo en el que podría aplicarse una optimización. Las reglas de reescritura de GHC que mencioné anteriormente son un gran ejemplo de un compilador que expone un mecanismo genérico para que las bibliotecas individuales las usen de la manera más adecuada para ellas.