Type-Driven Development pour un code sûr grâce aux types

• Les types constituent un contrat strict que les fonctions et les données doivent respecter
• Un type est un ensemble auquel certaines valeurs peuvent appartenir
• Les types peuvent être transformés via des fonctions, ce qui permet d’en modifier l’étendue
  • Fonction injective — transformer un type de petite étendue en un type de plus grande étendue
  • Fonction surjective — transformer un type de grande étendue en un type de plus petite étendue
  • Fonction bijective — correspondance un à un
• Il est possible de représenter les entrées et les sorties d’une logique par des types
  • Cela signifie qu’il est possible d’abstraire une logique à l’aide des types
  • On peut représenter les entrées et les sorties par des types, puis concevoir la logique à partir de cela
• On peut donner un nom à un type de données de base pour le distinguer comme un autre type
• En exploitant le système de types, on peut résoudre divers problèmes
  • Généralisation à l’aide des génériques
  • Restriction de domaine à l’aide des types fantômes
  • Restriction des comportements à l’aide des types union (ou types somme)
  • Gestion des TODO à l’aide d’un type minimal
  • Implémentation d’une machine à états finis à l’aide des types
  • Validation à l’aide des types dépendants
• Le développement piloté par les types est une méthodologie qui consiste à définir d’abord les types, puis à écrire le code à partir de ceux-ci
• Le développement piloté par les types peut être appliqué partout si on le souhaite, en commençant par définir en types le résultat de chaque étape
• Lors de l’analyse des exigences, il est utile d’essayer de les abstraire en types
• Même si le type de données de base est identique, s’il porte un sens différent, il vaut mieux le définir comme un type distinct pour le différencier
• Une fois les exigences analysées et les types envisagés, il est utile d’essayer d’abstraire la logique en types
  • Une abstraction du type (String) -> List<Token> est possible, par exemple
• Le développement piloté par les types se marie bien avec le développement piloté par les tests
  • Dans la mesure où l’on définit à l’avance les entrées et les résultats attendus avant d’écrire le code, le développement piloté par les types et le développement piloté par les tests se ressemblent
  • Si le développement piloté par les types permet de vérifier la sûreté à la compilation grâce au système de types, le développement piloté par les tests permet, lui, de détecter via du code de test les erreurs ou cas exceptionnels que les types seuls ne peuvent pas capturer
• Du point de vue du concepteur, exploiter le système de types revient à créer des règles de code pour les autres développeurs
• Toutefois, si l’on définit les types un à un au point d’en avoir trop, ou si leurs définitions deviennent trop complexes, cela peut au contraire rendre l’écriture du code plus difficile ou nuire à la lisibilité ; il est donc important de toujours maintenir un bon équilibre

[chabulhwi]

> Une fonction injective désigne le cas où l’ensemble des valeurs transformées ne coïncide pas entre le codomaine et l’image. Exprimé un peu plus simplement, cela signifie convertir d’un type de petite portée vers un type de plus grande portée.

Une fonction injective désigne une fonction dans laquelle les images de deux variables arbitraires distinctes sont différentes. Autrement dit, pour tous les éléments a et b appartenant au domaine X d’une fonction injective f, si a ≠ b, alors f(a) ≠ f(b). En mathématiques au lycée en Corée, ce qu’on appelle une « fonction un à un » correspond à une fonction injective.

[kciter1]

Merci pour ces explications détaillées. :) J’avais mal compris. C’est justement un point qu’on m’avait déjà signalé plusieurs fois, donc je vais approfondir un peu le sujet et réorganiser le contenu.