Pruebas o tipos

Hola Habr El otro día estaba buscando cómo hacer algo en Idris, y encontré una buena publicación, una traducción gratuita que parece bastante apropiada. Libertades y mordazas cuando sea necesario, denotaré "aquí por tales garabatos al principio y al final".

¿Cuándo usar pruebas y cuándo - tipos? ¿Qué información y qué garantías recibimos a cambio de nuestros esfuerzos para escribirlas?

Veremos un ejemplo simple y ligeramente inventado expresado en Python, C, Haskell e Idris. También veremos qué se puede decir sobre la implementación sin ningún conocimiento adicional al respecto, en cada caso.

No tomaremos en cuenta las diversas puertas traseras que nos permiten violar explícitamente las garantías del lenguaje (por ejemplo, extensiones C, unsafePerformIO inseguro en Haskell, conversiones de tipo inseguras), de lo contrario sería imposible sacar conclusiones, y esta publicación sería bastante corta. "Además, el mismo Haskell tiene un subconjunto de Safe Haskell que prohíbe explícita y transitivamente el uso de estos y otros trucos que podrían violar la integridad del lenguaje".

Especificación

Deja que se dé una lista y algún significado. Es necesario devolver el índice de este valor en la lista o indicar que este valor no está en la lista.

La implementación de esta especificación es trivial, por lo que es natural preguntar, y aquí hay generalmente pruebas o tipos. Sin embargo, esas propiedades y métodos de razonamiento, de los que hablaremos hoy, son aplicables a un código mucho más complejo. Deje que la implementación tome diez mil líneas de código de espagueti ilegible, si ayuda a ver su utilidad.

Pitón

 def x(y, z): # 10000    

Notamos de inmediato que no estamos interesados ​​en las propiedades no controladas ⟦y semánticas que no afectan a un programa como la denominación de variables y la documentación de texto, por lo que intencionalmente no escribí código que ayude a la percepción. Solo nos interesa el hecho de que, sujeto a pasar las pruebas y los controles de tipo, no puede ser falso .

En el código anterior, prácticamente no hay información útil más que el hecho de que tenemos una función que toma dos argumentos. Esta función también puede encontrar el índice del valor en la lista, o puede enviar una carta insultante a su abuela.

Análisis

No solo obtenemos código frágil sin pruebas y tipos, sino que nuestra única forma de entender lo que hace una función es la documentación. Y dado que la documentación es verificada por personas, no por máquinas, puede resultar desactualizada initially o inicialmente incorrecta⟧.

• La documentación
  
  • ✗ Conocemos el comportamiento esperado
    No tenemos nada que decirnos sobre el comportamiento de esta función. Odias a tu abuela. Eres un monstruo
• Garantías
  
  • ✓ Seguridad de memoria
    Python es un lenguaje de recolección de basura que elimina esta preocupación de nosotros. "Sin embargo, hasta donde yo sé, nada le impide extraer bibliotecas inseguras o C FFI dentro de esta función".

Python con pruebas

 def test_happy_path(): assert x([1, 2, 3], 2) == 1 def test_missing(): assert x([1, 2, 3], 4) is None 

Ahora sabemos que nuestra función funciona, y si falta el elemento, ¿el resultado es None ?

Pues no. Este es solo un ejemplo. Desafortunadamente, el alcance de nuestra función es infinito, y ningún número de ejemplos puede probar el funcionamiento correcto de nuestra función. Más pruebas: más confianza, pero ninguna cantidad de pruebas resolverá todas las dudas.

La posibilidad de que esta función devuelva None para 4 , pero no para 5 , suena más bien delirante, y en este caso particular, lo más probable es que no tenga sentido. Podemos estar satisfechos con nuestro nivel de fe y detenernos en un cierto número de ejemplos. Pero, de nuevo, la publicación será breve, así que imaginemos que la implementación no es tan obvia.

Como las pruebas no pueden probar algo en el caso general, sino que solo muestran el comportamiento con ejemplos específicos, las pruebas no pueden mostrar la ausencia de errores. Por ejemplo, no existe una prueba que muestre que nuestra función nunca arroja una excepción o nunca ingresa al ciclo eterno, o no contiene enlaces no válidos. Esto solo puede ser un análisis estático.

Sin embargo, incluso si los ejemplos no son muy buenos en el papel de la evidencia, al menos constituyen una buena documentación. De estos dos ejemplos podemos derivar la especificación completa full bajo algunos supuestos adicionales a priori: esos dos ejemplos también satisfacen, por ejemplo, la "contraespecificación" "encontrar el elemento en la matriz y devolver el anterior, si lo hay", lo que me llevó diez segundos para inventar .

Análisis

Aunque las pruebas pueden mostrar cómo usar nuestra función, y también dan un poco de confianza de que esta función funciona correctamente con al menos algunos ejemplos, no pueden probar nada sobre nuestro código en el caso general. Desafortunadamente, esto significa que las pruebas solo ayudan parcialmente a evitar errores.

• La documentación
  
  • ✓ Tenemos un ejemplo de uso
  • ✓ Conocemos algunas clases de valores que se procesarán correctamente
  • ✗ Conocemos todos los tipos de valores que se procesarán correctamente
    No tenemos restricciones sobre los tipos de argumentos, por lo que a pesar de la existencia de ejemplos de lo que puede manejar la función, no sabemos qué tipos no se han probado.
  • ✗ Conocemos el comportamiento esperado
    ⟦El autor del artículo original marcó aquí, me permitiré poner una cruz, dado el comentario anterior⟧
• Especificación
  
  • ✓ Funciona en al menos un caso
  • ✗ El índice devuelto siempre es un índice válido
  • ✗ El índice devuelto siempre indica un valor adecuado
  • ✗ El elemento faltante siempre devuelve None / Nothing
• Errores comunes
  
  • ✗ Sin errores tipográficos o nombres incorrectos
    El análisis estático puede ayudar, pero dado que Python es un lenguaje dinámico con la capacidad de anular varias cosas en tiempo de ejecución, nunca podemos probar que no haya errores.
    En particular, puede ser muy difícil o imposible determinar si el nombre del método es correcto, ya que la validez de la llamada al método depende del tipo de tiempo de ejecución del objeto en el que se realiza la llamada.
  • ✗ No null inesperado
  • ✗ El caso de error siempre se maneja
    En mi experiencia, esta es una de las fuentes más comunes de errores: en nuestro ejemplo, la función devuelve None en caso de que falte un elemento, pero el código que usa esta función puede suponer, por ejemplo, que siempre devolverá un número. Además, esto también puede conducir a una excepción no controlada.
• Garantías
  
  • ✓ Seguridad de memoria
  • ✗ La función no se puede llamar con el tipo incorrecto
  • ✗ Sin efectos secundarios
  • ✗ Sin excepciones
  • ✗ Sin errores
  • ✗ Sin ciclos perpetuos

Haskell

 xyz = -- 10000   

Si no está familiarizado con la sintaxis: esta es la definición de una función x con los parámetros y y z . En Haskell, puede omitir tipos, ya que se deducirán de la implementación ⟦a menos que, por supuesto, utilice diferentes funciones avanzadas de las extensiones modernas del sistema de tipos⟧.

Puede parecer que esto no es muy diferente de la versión de Python, pero solo gracias al hecho de que escribimos nuestra función en Haskell y está en mosaico, ya podemos hablar de algunas propiedades interesantes.

Análisis

Obviamente, no podemos sacar tantas conclusiones aquí, pero aquí hay algunos puntos a tener en cuenta:

• La documentación
  
  • ✗ Conocemos el comportamiento esperado
• Errores comunes
  
  • ✓ Sin errores tipográficos o nombres incorrectos
    Dado que Haskell es un lenguaje compilado, todos los nombres deben resolverse en el momento de la compilación. El programa simplemente no se compilará si hay este error.
  • ✓ Sin null inesperados
    Haskell simplemente no tiene null . ¡El problema está resuelto!
• Garantías
  
  • ✓ Seguridad de memoria
  • ✓ La función no se puede llamar con el tipo incorrecto
  • ✓ Sin efectos secundarios inesperados
    "El autor del artículo original no especificó este elemento, pero me permitiré señalar que si hay efectos secundarios, el tipo deducido de esta función indicará su presencia, de modo que el código de llamada conocerá sus capacidades".

Tipo de Haskell que especifica

 x :: Eq a => [a] -> a -> Maybe Int xyz = -- ... 

Anteriormente, hablamos de una actitud bastante intrigante hacia la seguridad de las abuelas: las pruebas dejaron claro que la función no iba a dañar a nadie, pero ¿ estaba realmente segura la abuela? ¿Esta función no envía letras juradas con precisión?

Haskell es conocido por ser un lenguaje funcional puro. Esto no significa que el código no pueda tener efectos secundarios, pero todos los efectos secundarios deben estar presentes en el tipo. Sabemos el tipo de esta función, vemos que está limpia, por lo que estamos seguros de que esta función no modifica ningún estado externo.

Esta es una propiedad muy interesante por otras razones: como sabemos que no hay efectos secundarios, podemos entender lo que hace esta función, ¡solo en función de su firma! Simplemente busque esta firma de Hoogle y mire el primer resultado. Por supuesto, esta no es la única función posible que tendría un tipo de este tipo, pero el tipo nos da suficiente confianza para los fines de la documentación.

Análisis

• La documentación
  
  • ✓ Conocemos el comportamiento esperado
  • ✗ Tenemos un ejemplo de uso
  • ✓ Conocemos algunas clases de valores que se procesarán correctamente
  • ✓ Conocemos todos los tipos de valores que se procesarán correctamente
• Especificación
  
  • ✗ Funciona en al menos un caso.
    Si faltan pruebas o pruebas, ¡no sabemos si nuestra función funciona como esperamos!
  • Index El índice devuelto es siempre un índice válido.
  • Index El índice devuelto siempre indica un valor adecuado.
  • Item Un elemento que falta siempre devuelve None / Nothing .
• Errores comunes
  
  • ✓ Sin errores tipográficos o nombres incorrectos
  • ✓ Sin null inesperados
  • ✓ El caso de error siempre se maneja
    Si nuestra función devuelve Nothing , entonces el sistema de tipos se asegura de que este caso sea manejado correctamente por el código de llamada. Por supuesto, este caso puede ser ignorado, pero esto debe hacerse explícitamente.
• Garantías
  
  • ✓ Seguridad de memoria
  • ✓ La función no se puede llamar con el tipo incorrecto
  • ✓ Sin efectos secundarios
  • ✗ Sin excepciones
    Comparto excepciones y errores, creyendo que después de las excepciones es posible recuperar, y después de los errores (por ejemplo, funciones parcialmente definidas) - no.
    En su mayor parte, las excepciones se describen en tipos (por ejemplo, en la mónada IO). En el buen sentido, debemos saber que una función no arrojará una excepción, solo en función de su tipo. Sin embargo, Haskell rompe esta expectativa al permitir que se generen excepciones desde el código puro .
    "Además, vale la pena señalar que en Haskell, los errores como llamar incorrectamente a funciones parcialmente definidas también se presentan como excepciones que pueden detectarse y procesarse, por lo que la diferencia entre las dos categorías es un poco menos obvia".
  • ✗ Sin errores
    Todavía podemos usar funciones parcialmente definidas, por ejemplo, división por cero.
  • ✗ Sin ciclos perpetuos

Haskell con pruebas

¿Recuerdas que dije antes que las pruebas no pueden probar la ausencia de errores? Mentí Cuando las estrellas convergen correctamente, y si las pruebas se combinan con tipos, ¡entonces es posible! La primera estrella es la finitud del dominio de nuestra función. El segundo: el dominio de la definición no solo debe ser finito, sino también no muy grande, de lo contrario, tal prueba será difícil de poner en práctica.

Por ejemplo:

 not :: Bool -> Bool not x = ... 

La entrada puede ser True o False . Es suficiente para probar estas dos opciones, y aquí está, ¡el Santo Grial! Sin excepciones, ciclos perpetuos, resultados incorrectos, sin errores. ⟦Sin embargo, para una función un poco más compleja, puede que no esté claro cuánto tiempo se dedica a las pruebas: si tardan mucho en completarse, ¿acabamos en un ciclo eterno, o es simplemente pesado? El problema de detenerla.

De hecho, esto tampoco es del todo cierto en el caso de Haskell: en cada tipo de Haskell también hay un valor ⊥ (que puede obtenerse como undefined , error o error en cierto sentido, como recursión infinita), pero los Haskellistas tradicionalmente cierran los ojos y creen que No existe.

Lectura extracurricular: solo hay cuatro mil millones de flotadores, ¡así que pruébelos todos!

En cualquier caso, en nuestro ejemplo original, el alcance es infinito, por lo que las pruebas solo pueden mostrar que nuestro código funciona para un conjunto finito de ejemplos.

Análisis
En este caso, las pruebas complementan los tipos y tapan algunos agujeros en el sistema de tipos Haskell. Tenemos mucha más confianza en nuestro código en comparación con el uso de solo pruebas o tipos.

C

 /* C    ,    int */ int x(int *y, size_t n, int z) { /* 10000    */ } 

Consideramos C fuera de interés en sistemas de tipos más antiguos. En C, en particular, los tipos probablemente no sean necesarios para el programador, sino para el compilador para ayudarlo a generar un código más rápido.

En nuestro ejemplo, no sabemos qué devolverá la función si no se encuentra el elemento. Tendremos que confiar en la tradición o en la documentación (por ejemplo, en este caso puede ser -1 ).

También podríamos usar argumentos: de esta manera podemos devolver un error y almacenar el valor de retorno en este argumento de salida. Esta es una opción un poco más expresiva, pero aún tenemos que confiar en la documentación para comprender qué parámetros se leen y cuáles se escriben. En ambos casos, es difícil entender el comportamiento al observar los tipos.

 /*   ,   out- */ error_t x(int *y, size_t n, int z, size_t *w) { /* 10000    */ } 

Análisis
El sistema de tipos en sí no nos da tantas garantías. Por supuesto, obtenemos información de estos tipos, pero solo compárela con el caso Haskell.

Idris

 x : Eq x => List x -> x -> Maybe Int xyz = ... 

Esta función es del mismo tipo que en el caso de Haskell. Sin embargo, con un sistema de tipo más expresivo, podemos lograr más. La elección de los tipos puede hablar sobre la implementación.

 %default total x : Eq x => Vect nx -> x -> Maybe (Fin n) xyz = ... 

Este tipo puede leerse como "dame una lista de tamaño n y algún valor, y te devolveré un número menor que n o Nothing ". Esto asegura que la función devuelve un índice que obviamente no va más allá de los límites.

Además, esta función es total, es decir, el temporizador ha comprobado que siempre termina. Esto elimina los ciclos perpetuos y los errores.

Análisis

• Especificación
  
  • ✗ Funciona en al menos un caso.
  • ✓ El índice devuelto siempre es el índice correcto
  • ✗ El índice devuelto siempre indica un valor adecuado
  • ✗ El elemento faltante siempre devuelve None / Nothing
• Garantías
  
  • ✓ Seguridad de memoria
  • ✓ La función no se puede llamar con el tipo incorrecto
  • ✓ Sin efectos secundarios
  • ✗ Sin excepciones
  • ✓ Sin errores
  • ✓ Sin ciclos perpetuos

Idris con pruebas

Dado que el lenguaje tipo de Idris es tan expresivo como el lenguaje de sus términos ⟦(o más bien, su parte demostrablemente total)⟧, la diferencia entre la prueba y el tipo es borrosa:

 ex : x [1, 2, 3] 2 = Just 1 ex = Refl 

Esta función tiene un tipo bastante extraño x [1, 2, 3] 2 = Just 1 . Este tipo significa que para una verificación de tipo exitosa, el tipeador debe demostrar que x [1, 2, 3] 2 estructuralmente igual a Just 1 . ⟦En este caso, la prueba es trivial, ya que es suficiente para que el volquete normalice los términos en ambos lados del signo igual, lo que se hará en un tiempo finito debido a la totalidad de todas las funciones utilizadas, y que conducirá a un resultado único debido a Church-Rosser. Después de eso, uno puede usar la reflexividad de la igualdad, que es lo que Refl.

De hecho, escribimos una prueba de nivel de tipo.

Idris con evidencia

Para completar el análisis, podemos usar todo el poder de los tipos dependientes y probar nuestra implementación (ya que los tipos dependientes en Idris son equivalentes a un sistema lógico que incluye lógica constructiva de primer orden).

En particular, podemos probar propiedades que antes eran inalcanzables para nosotros:

 --      Eq  DecEq x : DecEq a => Vect na -> (y : a) -> Maybe (Fin n) xyz = ... --    ,       `x` findIndexOk : DecEq a => (y : Vect na) -> (z : a) -> case xyz of Just i => index iy = z Nothing => Not (Elem zy) findIndexOk yz = ... 

El tipo findIndexOk se puede leer como "para cualquier tipo a modo que tenga una comparación algorítmicamente decidible ( DecEq ), para cualquier vector y elementos de tipo a cualquier longitud n cualquier valor z tipo a : si xyz devuelve el índice i , entonces este índice yace z , pero si xyz devuelve Nothing , entonces no existe tal elemento en el vector ".

"Es interesante que el autor del artículo original le dé un tipo un poco más débil que el dado anteriormente".

¡Ahora tenemos todo capturado! ¿Cuáles son las desventajas? Bueno, escribir toda esta evidencia puede ser bastante difícil.

Comparación

Opinión

En mi opinión, el uso de un sistema de tipo moderno en sí mismo es más efectivo en términos de la relación de la información recibida y las garantías al esfuerzo realizado. Si desea escribir un código bastante confiable, los tipos se pueden condimentar con pruebas. Idealmente, al estilo de QuickCheck.

Con los tipos dependientes, la línea entre pruebas y tipos se vuelve menos obvia. Si está escribiendo software para Boeing o para marcapasos, puede ser útil escribir evidencia.