¿Por qué los programas funcionales tienen una correlación entre el éxito de la compilación y la corrección?

Llevo 4 años con tendencia a la programación funcional, desde que comencé a trabajar con LINQ. Recientemente, escribí un código C # funcional puro y noté, de primera mano, lo que he estado leyendo sobre los programas funcionales: que una vez que se compilan, tienden a ser correctos.

Traté de señalar por qué este es el caso, pero no he tenido éxito.

Una suposición es que al aplicar los principios OO, tiene una "capa de abstracción" que no está presente en los programas funcionales y esta capa de abstracción hace posible que los contratos entre objetos sean correctos mientras la implementación es incorrecta.

¿Alguien ha pensado en esto y ha llegado a la razón abstracta subyacente de la correlación entre el éxito de la compilación y la corrección del programa en la programación funcional?

Puedo escribir esta respuesta como alguien que prueba mucho las cosas, así que para mí la corrección no es solo lo que funciona, sino lo que funciona y es fácil de probar.

En muchos sentidos, la programación funcional es más restrictiva que la programación imperativa. Después de todo, ¡nada te impide nunca mutar una variable en C! De hecho, la mayoría de las características en los lenguajes FP son fáciles de hablar en términos de solo algunas características principales. ¡Todo se reduce a lambdas, aplicación de funciones y coincidencia de patrones!

Sin embargo, dado que hemos pagado el premio por adelantado, tenemos mucho menos con qué lidiar y tenemos muchas menos opciones sobre cómo las cosas pueden salir mal. Si eres un fanático de 1984, ¡la libertad es realmente esclavitud! Al usar 101 trucos diferentes para un programa, tenemos que razonar sobre las cosas como si cualquiera de estas 101 cosas pudiera suceder. Eso es realmente difícil de hacer como resulta :)

Si comienzas con tijeras de seguridad en lugar de una espada, correr es moderadamente menos peligroso.

Ahora miramos su pregunta: ¿cómo encaja todo esto en "se compila y funciona!" fenómenos. ¡Creo que gran parte de esto es la misma razón por la cual es fácil probar el código! Después de todo, cuando escribes software estás construyendo alguna prueba informal de que es correcto. Debido a esto, lo que cubren sus pruebas naturales onduladas a mano y la propia noción de corrección de los compiladores (verificación de tipos) es bastante.

A medida que agrega características e interacciones complicadas entre ellas, aumenta lo que no verifica el sistema de tipos. Sin embargo, su capacidad para construir pruebas informales no parece mejorar. Esto significa que hay más cosas que pueden pasar por su inspección inicial y deben ser detectadas más tarde.

¿Cuál es la razón abstracta subyacente de la correlación entre el éxito de la compilación y la corrección del programa en la programación funcional?

Estado mutable.

Los compiladores comprueban las cosas estáticamente. Se aseguran de que su programa esté bien formado y el sistema de tipos proporciona un mecanismo para tratar de garantizar que se permitan los valores correctos en los lugares correctos. El sistema de tipos también trata de garantizar que se permita el tipo correcto de semántica en los lugares correctos.

Tan pronto como su programa introduce el estado, esa última restricción se vuelve menos útil. No solo debe preocuparse por los valores correctos en los lugares correctos, sino que también debe tener en cuenta ese cambio de valor en puntos arbitrarios de su programa. Debe tener en cuenta la semántica de su código que cambia junto con ese estado.

Si está haciendo bien la programación funcional, no hay (o muy poco) estado mutable.

Sin embargo, existe cierto debate sobre la causa aquí: si los programas sin estado funcionan después de la compilación con mayor frecuencia porque el compilador puede detectar más errores o si los programas sin estado funcionan después de la compilación con mayor frecuencia porque ese estilo de programación produce menos errores.

Es probable que sea una mezcla de ambos en mi experiencia.

En pocas palabras, las restricciones significan que hay menos formas correctas de poner las cosas juntas, y las funciones de primera clase facilitan la factorización de elementos como las estructuras de bucle. Tome el ciclo de esta respuesta , por ejemplo:

for (Iterator<String> iterator = list.iterator(); iterator.hasNext();) {
    String string = iterator.next();
    if (string.isEmpty()) {
        iterator.remove();
    }
}

Esta es la única forma segura e imperativa en Java de eliminar un elemento de una colección mientras está iterando a través de él. Hay muchas formas en que se ven muy cerca, pero están equivocadas. Las personas que no conocen este método a veces recurren a formas complicadas para evitar el problema, como iterar a través de una copia.

No es terriblemente difícil hacer este genérico, por lo que funcionará en más que solo colecciones de Strings, pero sin funciones de primera clase, no puede reemplazar el predicado (la condición dentro del if), por lo que este código tiende a copiarse y pegarse y modificado ligeramente.

Combine funciones de primera clase que le brinden la capacidad de pasar el predicado como parámetro, con la restricción de inmutabilidad que lo hace muy molesto si no lo hace, y se le ocurren bloques de construcción simples como filter, como en este código Scala eso hace lo mismo:

list filter (!_.isEmpty)

Ahora piense en lo que el sistema de tipos comprueba por usted, en el momento de la compilación en el caso de Scala, pero estas comprobaciones también las realizan los sistemas de tipos dinámicos la primera vez que lo ejecuta:

• listdebe ser algún tipo de tipo que admita el filtermétodo, es decir, una colección.
• Los elementos de listdeben tener un isEmptymétodo que devuelva un valor booleano.
• La salida será una colección (potencialmente) más pequeña con el mismo tipo de elementos.

Una vez que se han verificado esas cosas, ¿qué otras formas le quedan al programador para arruinar? Accidentalmente olvidé el !, lo que causó una falla de caso de prueba extremadamente obvia. Ese es prácticamente el único error disponible para cometer, y solo lo cometí porque estaba traduciendo directamente del código que probó la condición inversa.

Este patrón se repite una y otra vez. Las funciones de primera clase le permiten refactorizar las cosas en pequeñas utilidades reutilizables con una semántica precisa, las restricciones como la inmutabilidad le dan el impulso para hacerlo, y la comprobación de tipo de los parámetros de esas utilidades deja poco espacio para arruinarlas.

Por supuesto, todo esto depende de que el programador sepa que la función de simplificación filterya existe, y que sea capaz de encontrarla o de reconocer el beneficio de crearla usted mismo. Intente implementar esto usted mismo en todas partes usando solo la recursión de cola, y estará de vuelta en el mismo barco de complejidad que la versión imperativa, solo que peor. El hecho de que pueda escribirlo de manera muy simple no significa que la versión simple sea obvia.

No creo que haya una correlación significativa entre la compilación de programación funcional y la corrección del tiempo de ejecución. Puede haber alguna correlación entre la compilación estáticamente tipada y la corrección del tiempo de ejecución, ya que al menos puede tener los tipos correctos, si no está emitiendo.

El aspecto del lenguaje de programación que de alguna manera puede correlacionar la compilación exitosa con la corrección del tipo de tiempo de ejecución, como usted describe, es la escritura estática, e incluso entonces, solo si no está debilitando el verificador de tipos con conversiones que solo se pueden afirmar en tiempo de ejecución (en entornos con valores o lugares fuertemente tipados, por ejemplo, Java o .Net) o nada (en entornos donde la información de tipo se pierde o con tipeo débil, por ejemplo, C y C ++).

Sin embargo, la programación funcional per se puede ayudar de otras maneras, como evitar los datos compartidos y el estado mutable.

Ambos aspectos juntos pueden tener una correlación significativa en la corrección, pero debe tener en cuenta que no tener errores de compilación y tiempo de ejecución no dice nada, estrictamente hablando, sobre la corrección en un sentido más amplio, ya que en el programa hace lo que se supone que debe hacer y falla rápidamente sobre entrada inválida o falla de tiempo de ejecución incontrolable. Para eso, necesita reglas comerciales, requisitos, casos de uso, aserciones, pruebas unitarias, pruebas de integración, etc. Al final, al menos en mi opinión, proporcionan mucha más confianza que la programación funcional, la escritura estática o ambas.

Explicación para los gerentes:

Un programa funcional es como una máquina grande donde todo está conectado, tubos, cables. [Un coche]

Un programa de procedimiento es como un edificio con habitaciones que contienen una pequeña máquina, almacenando productos parciales en contenedores, obteniendo productos parciales de otros lugares. [Una fábrica]

Entonces, cuando la máquina funcional ya encaja: está destinada a producir algo. Si se ejecuta un complejo de procedimiento, es posible que haya supervisado efectos específicos, introducido el caos, no garantizado el funcionamiento. Incluso si tiene una lista de verificación de que todo está correctamente integrado, hay tantos estados, situaciones posibles (productos parciales por ahí, cubos desbordados, faltantes), que las garantías son difíciles de dar.

Pero en serio, el código de procedimiento no especifica la semántica del resultado deseado tanto como el código funcional. Los programadores de procedimientos pueden escapar más fácilmente mediante códigos y datos circunstanciales, e introducir varias formas de hacer una cosa (algunas de ellas imperfectas). Por lo general, se crean datos extraños. ¿Los programadores funcionales pueden tardar más cuando el problema se vuelve más complejo?

Un lenguaje funcional de tipo fuerte todavía puede mejorar los datos y el análisis de flujo. Con un lenguaje de procedimiento, el objetivo de un programa a menudo debe definirse fuera del programa, como un análisis formal de corrección.