Tests vs Types - Version rouille

Il y a quelques jours, 0xd34df00d a publié la traduction de l' article , décrivant les informations possibles sur une fonction si nous l'utilisons comme une "boîte noire", sans essayer de lire son implémentation. Bien sûr, ces informations sont très différentes d'une langue à l'autre; dans l'article d'origine, quatre cas ont été examinés:

• Python - typage dynamique, presque aucune information de la signature, quelques indices sont obtenus par les tests;
• C - typage statique faible, un peu plus d'informations;
• Haskell - typage statique fort, avec des fonctions pures par défaut, beaucoup plus d'informations;
• Typing dépendant d'Idris, le compilateur peut prouver l'exactitude de la fonction.

"Voici C et il y a Haskell, et qu'en est-il de Rust?" - c'était la première question de la discussion suivante. La réponse est ici.

Rappelons d'abord la tâche:

Étant donné une liste de valeurs et une valeur, renvoyez l'index de la valeur dans la liste ou signifiez qu'elle n'est pas présente dans la liste.

Si quelqu'un ne veut pas ne veut pas tout lire, les exemples de code sont fournis dans la cour de récréation de Rust .
Sinon, commençons!

Recherche simple

La première approche sera la signature presque naïve, ne différant du code C que par certains éléments idiomatiques:

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

Que savons-nous de cette fonction? Eh bien, en fait - pas beaucoup. Bien sûr, l' Option<usize> comme valeur de retour est une grande amélioration par rapport à tout ce qui est fourni par C, mais il n'y a aucune information sur la sémantique de la fonction. En particulier, nous n'avons aucune garantie que les effets secondaires sont absents et aucun moyen de vérifier en quelque sorte le comportement souhaité.

Un test peut-il améliorer cela? Regardez ici:

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

Rien de plus, semble-t-il - toutes ces vérifications peuvent être identiques en Python (et, par anticipation, les tests ne seront d'aucune utilité pour l'ensemble de l'article).

Utilisez les génériques, Luke!

Mais est-il bon que nous n'utilisions que des numéros signés 32 bits? Le réparer:

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

Eh bien, c'est quelque chose! Maintenant, nous pouvons prendre n'importe quelle tranche, composée d'éléments de tout type comparable. Le polymorphisme explicite est presque toujours meilleur qu'implicite (bonjour, Python) et presque toujours meilleur alors pas de polymorphisme du tout (bonjour, C), non?

Bien que cette fonction puisse passer ce test de manière inattendue:

 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); } 

Cela fait allusion au seul point manquant, car la spécification veut que la fonction refl , en fait, renvoie toujours Some(0) . Bien sûr, tout cela est dû au comportement spécifique des types partiellement équivalents en général et des flotteurs en particulier.
Peut-être que nous voulons nous débarrasser de ce problème? Donc, nous allons simplement resserrer la limite sur le type El:

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

Maintenant, nous exigeons non seulement que le type soit comparable, - nous avons besoin que ces comparaisons soient des équivalences . Ceci, bien sûr, limite les types possibles à utiliser avec cette fonction, mais maintenant, la signature et les tests indiquent que le comportement doit correspondre à la spécification.

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

Comme avant, mais un peu plus strict

Mais maintenant, nous avons peut-être besoin de garanties supplémentaires. Ou nous voulons travailler sur la pile (et ne pouvons donc pas utiliser Vec ), mais nous devons généraliser notre code pour chaque taille de tableau possible. Ou nous voulons compiler la fonction optimisée pour chaque taille de réseau concret.

Quoi qu'il en soit, nous avons besoin d'un tableau générique - et il y a une caisse dans Rust, fournissant exactement cela .

Maintenant, voici notre code:

 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'en savons-nous? Nous savons que cette fonction prendra le tableau d'une taille particulière, reflétée dans son type (et sera compilée indépendamment pour chacune de ces tailles). Pour l'instant, ce n'est presque rien - les mêmes garanties ont été fournies lors de l'exécution par l'implémentation précédente.

Mais nous pouvons aller plus loin.

Arithmétique au niveau du type

L'article initial mentionnait plusieurs garanties fournies par Idris, impossibles à obtenir dans d'autres langues. L'un d'eux - et probablement le plus simple, car il n'implique pas de preuves ou de tests, juste un petit changement de type, - indique que la valeur de retour, si ce n'est Nothing , sera toujours inférieure à la longueur de la liste.

On dirait que les types dépendants - ou quelque chose comme eux - sont nécessaires pour une telle garantie, et nous ne pouvons pas obtenir la même chose de Rust, non?

Rencontrez le typenum . En l'utilisant, nous pouvons écrire notre fonction de la manière suivante:

 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 } 

"Quelle est cette magie noire?!" - vous pourriez demander. Et vous avez raison: le typenum est une magie noire, et toute tentative d'utilisation est encore plus magique.

Mais cette signature de fonction est assez concrète.

• Il faut un tableau d'El avec la taille Size et un El de plus.
• Il renvoie une option qui, s'il s'agit de certains,
  
  • contient un objet trait , basé sur le trait UnsignedLessThan<Size> ;
  • et UnsignedLessThan<T> est implémenté partout où Unsigned et IsLess<T> sont implémentés et IsLess<T> renvoie B1, c'est-à-dire vrai.

En d'autres termes, cette fonction est garantie de renvoyer un entier non signé inférieur à la taille du tableau (à proprement parler, elle renvoie l'objet trait, mais nous pouvons appeler la méthode as_usize et obtenir l'entier).

Je peux maintenant parler de deux mises en garde majeures:

1. Nous pouvons obtenir une perte de performances. Si cette fonction est en quelque sorte sur le chemin "chaud" du programme, les répartitions dynamiques constantes peuvent ralentir tout le processus. Ce n'est peut-être pas une grande préoccupation, en fait, mais il y en a une autre:
2. Pour que cette fonction soit compilée, nous devons soit écrire la preuve de son exactitude juste à l'intérieur, soit tromper le système de type avec des éléments unsafe . Le premier est assez complexe et le dernier ne fait que tricher.

Conclusion

Bien sûr, dans la pratique, nous utiliserons généralement la seconde approche (avec tranche générique) ou l'approche en spoiler (avec itérateur). Toutes les discussions ultérieures n'ont probablement aucun intérêt pratique et ne sont ici que comme un exercice avec des types.

Quoi qu'il en soit, le fait que le système de type Rust puisse émuler la fonctionnalité du système de type Idris plus fort, comme pour moi, est assez impressionnant en soi.