Il y a quelques jours, 0xd34df00d a publié ici une traduction d'un article qui décrit ce que vous pouvez apprendre sur une fonction dans différents langages, si vous la considérez comme une "boîte noire" sans utiliser d'informations sur son implémentation (mais, bien sûr, sans l'empêcher d'utiliser le compilateur). Bien sûr, les informations reçues dépendent beaucoup de la langue - quatre exemples ont été pris en compte dans l'article d'origine:
- Python - typé dynamiquement, informations minimales, seuls les tests donnent des indices;
- C - faiblement typé statiquement, pas beaucoup plus d'informations;
- Haskell - fortement typé statiquement, avec des fonctions pures, beaucoup plus d'informations;
- Idris est un langage avec des types dépendants, il y a suffisamment d'informations pour prouver l'exactitude de la fonction lors de la compilation.
"Il y a C, il y a Haskell, mais où est Rust?!" - aussitôt la question a été posée. La réponse est sous la coupe.
Rappelez-vous l'état du problème:
Qu'une liste et un sens soient donnés. Il est nécessaire de renvoyer l'index de cette valeur dans la liste ou d'indiquer que cette valeur n'est pas dans la liste.
Pour les impatients - toutes les options discutées ci-dessous peuvent être vues dans la cour de récréation de Rust .
C'est parti!
Recherche simple
Nous commencerons par une signature presque naïve, qui, en fait, ne diffère du code C que par certains éléments idiomatiques:
fn foo(x: &[i32], y: i32) -> Option<usize> {
Que savons-nous de cette fonctionnalité? Enfin ... pas vraiment, en fait. Bien sûr, avoir Option<usize> dans les valeurs de retour est bien mieux que ce que C nous a fourni, mais nous n'avons toujours aucune information sur la sémantique de la fonction. En particulier, rien ne garantit qu'il n'y aura pas d'effets secondaires, ni aucun moyen de vérifier le comportement attendu.
Un test correctement écrit peut-il corriger la situation? Nous regardons:
#[test] fn test() { assert_eq!(foo(&[1, 2, 3], 2), Some(1)); assert_eq!(foo(&[1, 2, 3], 4), None); }
En général, nous n'avons rien obtenu de nouveau - toutes les mêmes vérifications que nous pourrions facilement faire avec Python (et, à l'avenir, les tests ne donneront pratiquement rien à l'avenir).
Utilisez les génériques, Luke!
Mais est-ce vraiment bien que nous soyons obligés d'utiliser uniquement des numéros 32 bits signés? Le désordre. Nous réparons:
fn foo<El>(x: &[El], y: El) -> Option<usize> where El: PartialEq, {
Ouais! C'est déjà quelque chose. Maintenant, nous pouvons prendre des tranches, constituées de tous les éléments que nous pouvons comparer pour l'égalité. Le polymorphisme explicite est presque toujours meilleur qu'implicite et presque toujours meilleur que rien, n'est-ce pas?
Cependant, une telle fonction peut passer inopinément le test suivant pour nous:
fn refl<El: PartialEq + Copy>(el: El) -> Option<usize> { foo(&[el], el)
Cela indique immédiatement une faille de notre part, car selon la spécification d'origine, un tel appel devrait renvoyer Some(0) . Bien sûr, le problème ici est dû à la spécificité des types avec une comparaison partiellement définie en général et des flottants en particulier.
Supposons maintenant que nous voulons nous débarrasser d'un tel problème - pour cela, nous resserrons simplement les exigences pour le type El:
fn foo<El>(x: &[El], y: El) -> Option<usize> where El: Eq, {
Maintenant, nous exigeons non seulement la possibilité d'une comparaison pour l'égalité - nous exigeons que cette comparaison soit une relation d'équivalence . Cela rétrécit quelque peu la gamme des paramètres possibles, mais maintenant, les types et les tests suggèrent (quoique pas explicitement) que le comportement attendu devrait vraiment entrer dans la spécification.
Digression: on veut aller PLUS générique!Cette option n'est pas liée à la tâche initiale, mais, à mon avis, est une bonne illustration du principe: "être libéral dans ce que vous acceptez, être conservateur dans ce que vous faites". En d'autres termes: s'il existe une opportunité, sans compromettre l'ergonomie et les performances, de rendre le type de valeurs acceptées plus général - il est logique de le faire.
Considérez cette option:
fn foo<'a, El: 'a>(x: impl IntoIterator<Item = &'a El>, y: El) -> Option<usize> where El: Eq, {
Que savons-nous de cette fonction maintenant? Tout est le même, seulement maintenant il n'accepte pas une liste ou une tranche en entrée, mais un objet arbitraire, qui peut être fait pour donner alternativement des liens vers des objets de type El et les comparer avec celui recherché: l'analogue en Java, si je me souviens bien, était serait une fonction qui prend un Iterable<Comparable> .
Comme auparavant, seulement plus strict
Cependant, par exemple, les garanties offertes par le compilateur à des étapes déjà connues ne nous suffisent pas. Ou, disons, nous ne voulons pas (pour une raison ou une autre) entrer dans un tas, mais voulons travailler sur la pile, ce qui signifie que nous avons besoin d'un tableau au lieu d'un vecteur, mais en même temps, nous voulons que notre code soit généralisé à différentes tailles du tableau . Ou nous voulons que la fonction soit optimisée autant que possible pour chaque taille spécifique de la liste d'entrée.
En bref, nous avons besoin d'un tableau générique - et Rust a déjà un package qui le fournit textuellement .
Nous avons maintenant à notre disposition le code suivant:
use generic_array::{GenericArray, ArrayLength}; fn foo<El, Size>(x: GenericArray<El, Size>, y: El) -> Option<usize> where El: Eq, Size: ArrayLength<El>, {
Que savons-nous de ce code? Que la fonction prend un tableau d'une certaine taille fixe, reflétée dans son type (et compilée indépendamment pour chacune de ces tailles). Jusqu'à présent, cela ne change pas grand-chose - au final, exactement les mêmes garanties, non seulement au stade de la monomorphisation, mais au moment de l'exécution, à condition que la version précédente soit coupée.
Mais nous pouvons aller encore plus loin.
Type Arithmétique de niveau
L'article original mentionnait plusieurs garanties que nous avons reçues d'Idris et que nous ne pouvions obtenir de personne d'autre. L'un d'eux - et peut-être le plus simple, car pour cela vous n'avez même pas besoin d'écrire une preuve à part entière ou un test à part entière, mais seulement pour spécifier un peu le type - il dit que la valeur de retour, si elle existe (c'est-à-dire si ce n'est pas Nothing ), ne doit pas dépasser la longueur de la liste d'entrée.
Il semblerait que la condition nécessaire pour une telle garantie soit la présence de types dépendants, enfin, ou au moins une sorte de similitude, et il serait étrange d'attendre quelque chose comme ça de Rust, non?
Rencontre - typenum . Avec lui, notre fonction peut être représentée comme ceci:
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>, {
"Qu'est-ce que c'est que cette magie noire?!" - demandez-vous. Et vous aurez certainement raison: le typenum est cette magie noire, et les tentatives pour l'utiliser au moins d'une manière ou d'une autre sont doublement.
Néanmoins, la signature de cette fonction est assez claire.
- La fonction accepte un tableau d'éléments El de longueur Size et un élément de type El.
- La fonction renvoie une valeur Option qui, si elle est Some,
- Il s'agit d'un objet trait basé sur le type
UnsignedLessThan<T> , qui accepte le type Size comme paramètre; - à son tour, le
IsLess<T> UnsignedLessThan<T> IsLess<T> implémenté pour tous les types qui implémentent Unsigned et IsLess<T> pour lesquels IsLess<T> renvoie B1, c'est-à-dire vrai
En d'autres termes, de cette manière, nous avons écrit une fonction qui est garantie de renvoyer un nombre non négatif (non signé) plus petit que la taille d'origine du tableau (ou plutôt, bien sûr, elle retourne ce même objet trait, à partir duquel nous devrons appeler plus tard la méthode as_usize , garantie de renvoyer un tel nombre) .
Il y a exactement deux astuces dans cette approche:
- Nous pouvons sensiblement perdre en performance. Si soudain, pour une raison quelconque, une telle fonction se trouve dans la partie "chaude" du programme, le besoin constant d'appels dynamiques peut être l'une des opérations les plus lentes. Cependant, cet inconvénient n'est peut-être pas aussi important qu'il y paraît, mais il y en a un second:
- Pour que cette fonction soit compilée correctement, nous devrons soit écrire réellement à l'intérieur la preuve de l'exactitude de son travail, soit «tromper» le système de
unsafe travers unsafe . Le premier est trop compliqué pour l'article du vendredi, mais le second n'est qu'une arnaque.
Conclusion
Bien sûr, dans la pratique, dans de tels cas, soit la deuxième implémentation (réception d'une tranche de type arbitraire) soit l'implémentation sous un spoiler (réception d'un objet itérable) sera utilisée. Tous les arguments ultérieurs n'ont presque certainement aucun intérêt pratique et servent uniquement d'exercice pour travailler avec un système de type.
Néanmoins, le fait que le système de type Rust puisse être en mesure d'émuler l'une des caractéristiques du système de type Idris manifestement plus fort est, à mon avis, tout à fait indicatif.