En la programación funcional, ¿cómo se logra la modularidad a través de las leyes matemáticas?

Leí en esta pregunta que los programadores funcionales tienden a usar pruebas matemáticas para asegurarse de que su programa funciona correctamente. Esto suena mucho más fácil y rápido que las pruebas unitarias, pero viniendo de un fondo de OOP / Pruebas unitarias, nunca lo he visto hecho.

¿Me lo puedes explicar y darme un ejemplo?

Una prueba es mucho más difícil en el mundo de OOP debido a los efectos secundarios, la herencia sin restricciones y nullser miembro de todo tipo. La mayoría de las pruebas se basan en un principio de inducción para demostrar que ha cubierto todas las posibilidades, y las 3 cosas hacen que sea más difícil de probar.

Digamos que estamos implementando árboles binarios que contienen valores enteros (en aras de mantener la sintaxis más simple, no incluiré programación genérica en esto, aunque no cambiaría nada). En ML estándar, definiría eso como esta:

datatype tree = Empty | Node of (tree * int * tree)

Esto introduce un nuevo tipo llamado treecuyos valores pueden venir exactamente en dos variedades (o clases, que no deben confundirse con el concepto OOP de una clase): un Emptyvalor que no contiene información y Nodevalores que llevan una tupla 3 cuya primera y última los elementos son treesy cuyo elemento medio es an int. La aproximación más cercana a esta declaración en OOP se vería así:

public class Tree {
    private Tree() {} // Prevent external subclassing

    public static final class Empty extends Tree {}

    public static final class Node extends Tree {
        public final Tree leftChild;
        public final int value;
        public final Tree rightChild;

        public Node(Tree leftChild, int value, Tree rightChild) {
            this.leftChild = leftChild;
            this.value = value;
            this.rightChild = rightChild;
        }
    }
}

Con la advertencia de que las variables de tipo Árbol nunca pueden ser null.

Ahora escribamos una función para calcular la altura (o profundidad) del árbol, y supongamos que tenemos acceso a una maxfunción que devuelve el mayor de dos números:

fun height(Empty) =
        0
 |  height(Node (leftChild, value, rightChild)) =
        1 + max( height(leftChild), height(rightChild) )

Hemos definido la heightfunción por casos: hay una definición para Emptyárboles y una definición para Nodeárboles. El compilador sabe cuántas clases de árboles existen y emitiría una advertencia si no define ambos casos. La expresión Node (leftChild, value, rightChild)en la firma de la función une los valores de la 3-tupla a las variables leftChild, valuey rightChildrespectivamente, de manera que podemos hacer referencia a ellos en la definición de función. Es similar a haber declarado variables locales como esta en un lenguaje OOP:

Tree leftChild = tuple.getFirst();
int value = tuple.getSecond();
Tree rightChild = tuple.getThird();

¿Cómo podemos demostrar que hemos implementado heightcorrectamente? Podemos usar la inducción estructural , que consiste en: 1. Probar que heightes correcto en los casos base de nuestro treetipo ( Empty) 2. Suponiendo que las llamadas recursivas heightsean correctas, demuestre que heightes correcto para los casos no base ) (cuando el árbol es realmente a Node).

Para el paso 1, podemos ver que la función siempre devuelve 0 cuando el argumento es un Emptyárbol. Esto es correcto por definición de la altura de un árbol.

Para el paso 2, la función vuelve 1 + max( height(leftChild), height(rightChild) ). Suponiendo que las llamadas recursivas realmente devuelven la altura de los niños, podemos ver que esto también es correcto.

Y eso completa la prueba. Los pasos 1 y 2 combinados agotan todas las posibilidades. Tenga en cuenta, sin embargo, que no tenemos mutación, ni nulos, y que hay exactamente dos variedades de árboles. Elimine esas tres condiciones y la prueba rápidamente se vuelve más complicada, si no práctica.

EDITAR: Dado que esta respuesta ha llegado a la cima, me gustaría agregar un ejemplo menos trivial de una prueba y cubrir la inducción estructural un poco más a fondo. Arriba probamos que si heightdevuelve , su valor de retorno es correcto. Sin embargo, no hemos demostrado que siempre devuelva un valor. Podemos usar la inducción estructural para probar esto también (o cualquier otra propiedad). Nuevamente, durante el paso 2, se nos permite asumir las propiedades retenidas de las llamadas recursivas siempre que todas las llamadas recursivas operen en un hijo directo del árbol.

Una función puede fallar al devolver un valor en dos situaciones: si arroja una excepción y si se repite para siempre. Primero demostremos que si no se lanzan excepciones, la función termina:

1. Demuestre que (si no se lanzan excepciones) la función termina para los casos base ( Empty). Como incondicionalmente devolvemos 0, termina.

2. Probar que la función termina en los casos no base ( Node). Hay tres llamadas a funciones aquí: +, max, y height. Lo sabemos +y maxterminamos porque son parte de la biblioteca estándar del lenguaje y están definidos de esa manera. Como se mencionó anteriormente, se nos permite asumir que la propiedad que intentamos probar es verdadera en las llamadas recursivas siempre que operen en subárboles inmediatos, por lo que las llamadas heightfinalizarán también.

Eso concluye la prueba. Tenga en cuenta que no podrá probar la terminación con una prueba unitaria. Ahora todo lo que queda es mostrar que heightno arroja excepciones.

1. Probar que heightno arroja excepciones en el caso base ( Empty). Devolver 0 no puede arrojar una excepción, así que hemos terminado.
2. Probar que heightno arroja una excepción en el caso no base ( Node). Asuma una vez más que sabemos +y maxno arroje excepciones. Y la inducción estructural nos permite asumir que las llamadas recursivas tampoco se lanzarán (porque operan en los hijos inmediatos del árbol). ¡Pero esperen! Esta función es recursiva, pero no recursiva de cola . ¡Podríamos volar la pila! Nuestro intento de prueba ha descubierto un error. Podemos arreglarlo cambiando heightpara que sea recursivo en la cola .

Espero que esto muestre que las pruebas no tienen que ser aterradoras o complicadas. De hecho, cada vez que escribe un código, ha construido informalmente una prueba en su cabeza (de lo contrario, no estaría convencido de que acaba de implementar la función). Al evitar la mutación nula e innecesaria y la herencia sin restricciones, puede demostrar que su intuición es corregir con bastante facilidad. Estas restricciones no son tan duras como podría pensar:

• null es un defecto del idioma y eliminarlo es incondicionalmente bueno.
• La mutación a veces es inevitable y necesaria, pero se necesita con mucha menos frecuencia de lo que parece, especialmente cuando tiene estructuras de datos persistentes.
• En cuanto a tener un número finito de clases (en el sentido funcional) / subclases (en el sentido OOP) frente a un número ilimitado de ellas, ese es un tema demasiado grande para una sola respuesta . Baste decir que hay un intercambio de diseño allí: la probabilidad de corrección frente a la flexibilidad de extensión.

1. Es mucho más fácil razonar sobre el código cuando todo es inmutable . Como resultado, los bucles se escriben con mayor frecuencia como recursividad. En general, es más fácil verificar la corrección de una solución recursiva. A menudo, dicha solución también se leerá de manera muy similar a una definición matemática del problema.

   Sin embargo, hay muy poca motivación para llevar a cabo una prueba formal real de corrección en la mayoría de los casos. Las pruebas son difíciles, toman mucho tiempo (humano) y tienen un ROI bajo.

2. Algunos lenguajes funcionales (especialmente de la familia ML) tienen sistemas de tipos extremadamente expresivos que pueden ofrecer garantías mucho más completas que un sistema de tipos de estilo C (pero algunas ideas como los genéricos también se han vuelto comunes en los idiomas convencionales). Cuando un programa pasa una verificación de tipo, este es un tipo de prueba automatizada. En algunos casos, esto podrá detectar algunos errores (por ejemplo, olvidar el caso base en una recursión u olvidar manejar ciertos casos en una coincidencia de patrón).

   Por otro lado, estos sistemas de tipo deben mantenerse muy limitados para que sean decidibles . Entonces, en cierto sentido, obtenemos garantías estáticas al renunciar a la flexibilidad, y estas restricciones son una razón por la cual existen trabajos académicos complicados en la línea de " Una solución monádica a un problema resuelto, en Haskell ".

   Me gustan los idiomas muy liberales y los idiomas muy restringidos, y ambos tienen sus respectivas dificultades. Pero no es el caso de que uno sea "mejor", cada uno es más conveniente para un tipo diferente de tarea.

Luego hay que señalar que las pruebas y las pruebas unitarias no son intercambiables. Ambos nos permiten poner límites a la corrección del programa:

• Las pruebas ponen un límite superior a la corrección: si una prueba falla, el programa es incorrecto, si ninguna prueba falla, estamos seguros de que el programa manejará los casos probados, pero aún puede haber errores no descubiertos.

  int factorial(int n) {
    if (n <= 1) return 1;
    if (n == 2) return 2;
    if (n == 3) return 6;
    return -1;
  }
  
  assert(factorial(0) == 1);
  assert(factorial(1) == 1);
  assert(factorial(3) == 6);
  // oops, we forgot to test that it handles n > 3…
  

• Las pruebas ponen un límite inferior a la corrección: puede ser imposible probar ciertas propiedades. Por ejemplo, puede ser fácil demostrar que una función siempre devuelve un número (eso es lo que hacen los sistemas de tipos). Pero puede ser imposible demostrar que el número siempre será < 10.

  int factorial(int n) {
    return n;  // FIXME this is just a placeholder to make it compile
  }
  
  // type system says this will be OK…
  

Una palabra de advertencia puede estar en orden aquí:

Si bien es generalmente cierto lo que otros escriben aquí, en resumen, que los sistemas de tipos avanzados, la inmutabilidad y la transparencia referencial contribuyen mucho a la corrección, no es el caso que las pruebas no se realicen en el mundo funcional. Por el contrario !

Esto se debe a que tenemos herramientas como Quickcheck, que generan casos de prueba de forma automática y aleatoria. Simplemente establece las leyes que una función debe obedecer, y luego la verificación rápida verificará estas leyes para cientos de casos de prueba aleatorios.

Verá, este es un nivel un poco más alto que las verificaciones de igualdad triviales en un puñado de casos de prueba.

Aquí hay un ejemplo de una implementación de un árbol AVL:

--- A generator for arbitrary Trees with integer keys and string values
aTree = arbitrary :: Gen (Tree Int String)


--- After insertion, a lookup with the same key yields the inserted value        
p_insert = forAll aTree (\t -> 
             forAll arbitrary (\k ->
               forAll arbitrary (\v ->
                lookup (insert t k v) k == Just v)))

--- After deletion of a key, lookup results in Nothing
p_delete = forAll aTree (\t ->
            not (null t) ==> forAll (elements (keys t)) (\k ->
                lookup (delete t k) k == Nothing))

La segunda ley (o propiedad) podemos leer lo siguiente: para todos los árboles arbitrarios t, se cumple lo siguiente: si tno está vacío, entonces, para todas las claves kde ese árbol, se mantendrá esa búsqueda ken el árbol que es el resultado de eliminar kdesde t, el resultado será Nothing(que indica: no encontrado).

Esto verifica la funcionalidad adecuada para la eliminación de una clave existente. ¿Qué leyes deberían regir la eliminación de una clave no existente? Ciertamente queremos que el árbol resultante sea el mismo que el que eliminamos. Podemos expresar esto fácilmente:

p_delete_nonexistant = forAll aTree (\t ->
                          forAll arbitrary (\k -> 
                              k `notElem` keys t ==> delete t k == t))

De esta manera, las pruebas son realmente divertidas. Y además, una vez que aprende a leer las propiedades de la comprobación rápida, sirven como una especificación comprobable por máquina .

No entiendo exactamente qué significa la respuesta vinculada al "lograr la modularidad a través de las leyes matemáticas", pero creo que tengo una idea de lo que significa.

Echa un vistazo a Functor :

La clase Functor se define así:

 class Functor f where
   fmap :: (a -> b) -> f a -> f b

No viene con casos de prueba, sino con un par de leyes que deben cumplirse.

Todas las instancias de Functor deben obedecer:

 fmap id = id
 fmap (p . q) = (fmap p) . (fmap q)

Ahora supongamos que implementa Functor( fuente ):

instance  Functor Maybe  where
    fmap _ Nothing       = Nothing
    fmap f (Just a)      = Just (f a)

El problema es verificar que su implementación cumpla con las leyes. ¿Cómo haces para hacer eso?

Un enfoque es escribir casos de prueba. La limitación fundamental de este enfoque es que está verificando el comportamiento en un número finito de casos (¡buena suerte probando exhaustivamente una función con 8 parámetros!), Por lo que pasar las pruebas no puede garantizar nada más que que las pruebas pasen.

Otro enfoque es utilizar el razonamiento matemático, es decir, una prueba, basada en la definición real (en lugar de en el comportamiento en un número limitado de casos). La idea aquí es que una prueba matemática puede ser más efectiva; sin embargo, esto depende de qué tan adecuado sea su programa para la prueba matemática.

No puedo guiarlo a través de una prueba formal real de que la Functorinstancia anterior cumple con las leyes, pero intentaré dar un resumen de cómo se vería la prueba:

1. fmap id = id
   • si tenemos Nothing
     • fmap id Nothing= Nothingpor parte 1 de la implementación
     • id Nothing= Nothingpor la definición deid
   • si tenemos Just x
     • fmap id (Just x)= Just (id x)= Just xpor la parte 2 de la implementación, luego por la definición deid
2. fmap (p . q) = (fmap p) . (fmap q)
   • si tenemos Nothing
     • fmap (p . q) Nothing= Nothingpor parte 1
     • (fmap p) . (fmap q) $ Nothing= (fmap p) $ Nothing= Nothingpor dos aplicaciones de la parte 1
   • si tenemos Just x
     • fmap (p . q) (Just x)= Just ((p . q) x)= Just (p (q x))por la parte 2, luego por la definición de.
     • (fmap p) . (fmap q) $ (Just x)= (fmap p) $ (Just (q x))= Just (p (q x))por dos aplicaciones de la segunda parte

"Tenga cuidado con los errores en el código anterior; solo he demostrado que es correcto, no lo he probado". - Donald Knuth

En un mundo perfecto, los programadores son perfectos y no cometen errores, por lo que no hay errores.

En un mundo perfecto, los informáticos y los matemáticos también son perfectos, y tampoco cometen errores.

Pero no vivimos en un mundo perfecto. Por lo tanto, no podemos confiar en que los programadores no cometan errores. Pero no podemos suponer que ningún informático que presente una prueba matemática de que un programa es correcto no cometió ningún error en esa prueba. Así que no le prestaría atención a nadie que intente probar que su código funciona. Escriba pruebas unitarias y muéstreme que el código se comporta de acuerdo con las especificaciones. Cualquier otra cosa no me convencerá de nada.