Pruebas vs. Tipos: versión de óxido

Hace unos días, 0xd34df00d publicó la traducción del artículo , describiendo la posible información sobre alguna función si la usamos como un "recuadro negro", sin tratar de leer su implementación. Por supuesto, esta información es bastante diferente de un idioma a otro; En el artículo original, se consideraron cuatro casos:

• Python: escritura dinámica, casi sin información de la firma, las pruebas obtienen algunas pistas;
• C - escritura estática débil, un poco más de información;
• Haskell - fuerte tipeo estático, con funciones puras por defecto, mucha más información;
• Idris - mecanografía dependiente, el compilador puede probar la corrección de la función.

"Aquí está C y está Haskell, ¿y qué hay de Rust?" - Esta fue la primera pregunta en la siguiente discusión. La respuesta está aquí.

Primero recordemos la tarea:

Dada una lista de valores y un valor, devuelve el índice del valor en la lista o significa que no está presente en la lista.

Si alguien no quiere no quiere leer todo esto, los ejemplos de código se proporcionan en el área de juegos de Rust .
De lo contrario, ¡comencemos!

Búsqueda simple

El primer enfoque será la firma casi ingenua, que difiere del código C solo en algunos elementos idiomáticos:

fn foo(x: &[i32], y: i32) -> Option<usize> { // Implementation elided } 

¿Qué sabemos sobre esta función? Bueno, de hecho, no mucho. Por supuesto, la Option<usize> como valor de retorno es una gran mejora sobre lo que sea proporcionado por C, pero no hay información sobre la semántica de la función. En particular, no tenemos garantía de que los efectos secundarios estén ausentes y no hay forma de verificar de alguna manera el comportamiento deseado.

¿Puede una prueba mejorar esto? Mira aquí:

 #[test] fn test() { assert_eq!(foo(&[1, 2, 3], 2), Some(1)); assert_eq!(foo(&[1, 2, 3], 4), None); } 

Parece que nada más: todas estas comprobaciones pueden ser las mismas en Python (y, con anticipación, las pruebas serán de poca ayuda para todo el artículo).

¡Usa los genéricos, Luke!

¿Pero es bueno que tengamos que usar solo números con signo de 32 bits? Arreglando:

 fn foo<El>(x: &[El], y: El) -> Option<usize> where El: PartialEq, { // Implementation elided } 

Bueno, eso es algo! Ahora podemos tomar cualquier porción, que consta de elementos de cualquier tipo comparable. El polimorfismo explícito es casi siempre mejor que implícito (hola, Python) y casi siempre mejor que ningún polimorfismo (hola, C), ¿verdad?

Aunque, esta función puede pasar inesperadamente esta prueba:

 fn refl<El: PartialEq + Copy>(el: El) -> Option<usize> { foo(&[el], el) // should always return Some(0), right? } #[test] fn dont_find_nan() { assert_eq!(refl(std::f64::NAN), None); } 

Esto sugiere el único punto que falta, ya que la especificación quiere que la función refl , de hecho, siempre devuelva Some(0) . Por supuesto, todo esto se debe al comportamiento específico de los tipos parcialmente equivalentes en general y flotantes en particular.
¿Quizás queremos deshacernos de este problema? Entonces, simplemente ajustaremos el límite en el tipo El:

 fn foo<El>(x: &[El], y: El) -> Option<usize> where El: Eq, { // Implementation elided } 

Ahora, estamos exigiendo que no solo el tipo sea comparable, sino que exigimos que estas comparaciones sean equivalencias . Esto, por supuesto, limita los tipos posibles para usar con esta función, pero ahora tanto la firma como las pruebas sugieren que el comportamiento debería encajar en la especificación.

 fn foo<'a, El: 'a>(x: impl IntoIterator<Item = &'a El>, y: El) -> Option<usize> where El: Eq, { // Implementation elided } 

Como antes, pero un poco más estricto

Pero ahora, tal vez necesitamos algunas garantías más. O queremos trabajar en la pila (y no podemos usar Vec ), pero necesitamos generalizar nuestro código para cada tamaño de matriz posible. O queremos compilar la función optimizada para cada tamaño de matriz concreta.

De todos modos, necesitamos una matriz genérica, y hay una caja en Rust, que proporciona exactamente eso .

Ahora, aquí está nuestro código:

 use generic_array::{GenericArray, ArrayLength}; fn foo<El, Size>(x: GenericArray<El, Size>, y: El) -> Option<usize> where El: Eq, Size: ArrayLength<El>, { // Implementation elided } 

¿Qué sabemos de él? Sabemos que la función tomará la matriz de un tamaño particular, reflejada en su tipo (y se compilará de forma independiente para cada tamaño). Por ahora, esto no es casi nada: las mismas garantías fueron proporcionadas en tiempo de ejecución por la implementación anterior.

Pero podemos llegar más lejos.

Aritmética de nivel de tipo

El artículo inicial mencionaba varias garantías proporcionadas por Idris que eran imposibles de obtener de otros idiomas. Uno de ellos, y probablemente el más simple, ya que no implica ninguna prueba o prueba, solo un pequeño cambio en los tipos, afirma que el valor de retorno, si no es Nothing , siempre será menor que la longitud de la lista.

Parece que los tipos dependientes, o algo así, son necesarios para tal garantía, y no podemos obtener lo mismo de Rust, ¿verdad?

Conoce al typenum . Al usarlo, podemos escribir nuestra función de la siguiente manera:

 use generic_array::{ArrayLength, GenericArray}; use typenum::{IsLess, Unsigned, B1}; trait UnsignedLessThan<T> { fn as_usize(&self) -> usize; } impl<Less, More> UnsignedLessThan<More> for Less where Less: IsLess<More, Output = B1>, Less: Unsigned, { fn as_usize(&self) -> usize { <Self as Unsigned>::USIZE } } fn foo<El, Size>(x: GenericArray<El, Size>, y: El) -> Option<Box<dyn UnsignedLessThan<Size>>> where El: Eq, Size: ArrayLength<El>, { // Implementation elided } 

"¡¿Qué es esta magia negra ?!" - podrías preguntar. Y tienes razón: typenum es una magia negra, y cualquier intento de usarla es aún más mágica.

Pero esta firma de función es bastante concreta.

• Se necesita una variedad de El con la longitud Tamaño y un El más.
• Devuelve una Opción que, si es Some,
  
  • contiene un objeto de rasgo , basado en el rasgo UnsignedLessThan<Size> ;
  • y UnsignedLessThan<T> se implementa dondequiera que se implementen Unsigned e IsLess<T> y IsLess<T> devuelve B1, es decir, verdadero.

En otras palabras, se garantiza que esta función devolverá un entero sin signo menor que el tamaño de la matriz (estrictamente hablando, devuelve el objeto rasgo, pero podemos llamar as_usize método as_usize y obtener el entero).

Ahora puedo hablar de dos advertencias principales:

1. Podemos tener una pérdida de rendimiento. Si de alguna manera esta función estará en la ruta "activa" del programa, los despachos dinámicos constantes podrían ralentizar todo el proceso. Esto podría no ser una gran preocupación, de hecho, pero hay otra:
2. Para que esta función se compile, debemos escribir la prueba de su corrección dentro de ella o engañar al sistema de tipos con algo unsafe . El primero es bastante complejo, y el segundo es solo hacer trampa.

Conclusión

Por supuesto, en la práctica usaremos generalmente el segundo enfoque (con corte genérico) o el enfoque en spoiler (con iterador). Probablemente, toda discusión posterior no sea de ningún interés práctico y es aquí solo como un ejercicio con tipos.

De todos modos, el hecho de que el sistema de tipo Rust puede emular la característica del sistema de tipo Idris más fuerte, en mi opinión, es bastante impresionante en sí mismo.