Idris2 est une sorte d'Haskell en plus poussé. La version 2 s'appuie sur la « Quantitative Type Theory ». Ça permet d'écrire des mettre des nombres dans les types, comme ...
Je n'ai pas vraiment réussi à comprendre ce que ça apportait en pratique pour les développeurs. Et je n'ai pas été spécialement été attiré par ce que j'ai vu. C'est probablement très intéressant, mais je ne dois pas être la bonne personne pour ça.
"Ecrire des nombres dans les types" ce n'est pas nouveau, cela se fait depuis des années dans de nombreux langages. C++ par exemple te permet d'avoir des nombres au niveau du type. Haskell fait cela très bien aussi. Idris apporte cependant plus de confort sur des cas plus avancés, que je ne détaillerais pas ici.
Ecrire des nombres dans des types peut permettre de rendre des interfaces plus robustes avec des vérifications à la compilation. L'exemple canon c'est celui des vecteurs que tu as donné, qui permet par exemple d’empêcher (à la compilation) les accès à des cases qui n'existe pas. Un autre exemple serait la multiplication de matrice : celle-ci ne fonctionne normalement qu'avec des matrices ayant des tailles en correspondance. En gros, multiplier une matrice de taille "N * M" avec une matrice de taille "N' * M'" donne une matrice de taille "N * M'". À partir du moment ou tu es sensibilisé à ce type de pratique, tu commences à voir des cas d'application partout. En réseau, tu peux imaginer avoir un tag dans ton type de socket pour connaitre son état actuel, et ainsi empêcher des cas impossibles. Tu peux imaginer ajouter l'unité d'une grandeur physique afin de refuser d'ajouter des mètres et des grammes. Tu peux imaginer une librairie de gestion de chemin de fichier qui sait (à la compilation) si le chemin est absolu ou relatif. Une librairie de gestion de couleur qui n’autorise que les traitements dans des espaces colorimétriques compatibles. Une librairie de géométrie qui interdit des opérations mal définie (addition de deux positions. Translation d'une position en deux dimension par un vecteur 3 dimensions). Si tu as une libraire de dessin (type cairo) avec plusieurs backend supportant chacun différentes fonctionnalités, tu peux imaginer que le type final de ton dessin "liste" les fonctionnalités nécessaires et refuse (à la compilation) de générer une sortie si le backend n'en est pas capable. Si tu fais du web, tu peux imaginer un langage au dessus de CSS / HTML qui s'assure (à la compilation) que tu n'a pas d'incohérence dans les noms de tes classes CSS. Tu peux aussi vérifier (à la compilation) que tous tes liens internes de ton site web pointent vers des ressources qui existent.
La liste est infinie, le but est encore une fois d’empêcher de compiler des programmes qui ne sont pas correctes. Tout ce que tu peux exprimer au niveau du type c'est des erreurs en moins à l’exécution et des tests en moins à faire. C'est un compromis à évaluer en fonction de trop nombreux paramètres : comme ton aisance avec le langage, la simplicité de celui-ci, l'impact sur le temps de développement, l'impact d'une erreur runtime en production, l'impact sur l'évolution future du code. Ce n'est pas facile à évaluer ;)
# Nombre dans les types
Posté par Guillaum (site web personnel) . En réponse au journal Explorer des langages de programmation - édition 2020. Évalué à 8.
"Ecrire des nombres dans les types" ce n'est pas nouveau, cela se fait depuis des années dans de nombreux langages. C++ par exemple te permet d'avoir des nombres au niveau du type. Haskell fait cela très bien aussi. Idris apporte cependant plus de confort sur des cas plus avancés, que je ne détaillerais pas ici.
Ecrire des nombres dans des types peut permettre de rendre des interfaces plus robustes avec des vérifications à la compilation. L'exemple canon c'est celui des vecteurs que tu as donné, qui permet par exemple d’empêcher (à la compilation) les accès à des cases qui n'existe pas. Un autre exemple serait la multiplication de matrice : celle-ci ne fonctionne normalement qu'avec des matrices ayant des tailles en correspondance. En gros, multiplier une matrice de taille "N * M" avec une matrice de taille "N' * M'" donne une matrice de taille "N * M'". À partir du moment ou tu es sensibilisé à ce type de pratique, tu commences à voir des cas d'application partout. En réseau, tu peux imaginer avoir un tag dans ton type de socket pour connaitre son état actuel, et ainsi empêcher des cas impossibles. Tu peux imaginer ajouter l'unité d'une grandeur physique afin de refuser d'ajouter des mètres et des grammes. Tu peux imaginer une librairie de gestion de chemin de fichier qui sait (à la compilation) si le chemin est absolu ou relatif. Une librairie de gestion de couleur qui n’autorise que les traitements dans des espaces colorimétriques compatibles. Une librairie de géométrie qui interdit des opérations mal définie (addition de deux positions. Translation d'une position en deux dimension par un vecteur 3 dimensions). Si tu as une libraire de dessin (type cairo) avec plusieurs backend supportant chacun différentes fonctionnalités, tu peux imaginer que le type final de ton dessin "liste" les fonctionnalités nécessaires et refuse (à la compilation) de générer une sortie si le backend n'en est pas capable. Si tu fais du web, tu peux imaginer un langage au dessus de CSS / HTML qui s'assure (à la compilation) que tu n'a pas d'incohérence dans les noms de tes classes CSS. Tu peux aussi vérifier (à la compilation) que tous tes liens internes de ton site web pointent vers des ressources qui existent.
La liste est infinie, le but est encore une fois d’empêcher de compiler des programmes qui ne sont pas correctes. Tout ce que tu peux exprimer au niveau du type c'est des erreurs en moins à l’exécution et des tests en moins à faire. C'est un compromis à évaluer en fonction de trop nombreux paramètres : comme ton aisance avec le langage, la simplicité de celui-ci, l'impact sur le temps de développement, l'impact d'une erreur runtime en production, l'impact sur l'évolution future du code. Ce n'est pas facile à évaluer ;)