Algèbre des types : produits et sommes

La théorie des types algébriques nous offre une correspondance élégante entre les structures de données et l’arithmétique élémentaire.

Les types produits

Un product type, c’est-à-dire une structure, un tuple ou un record, représente une conjonction  : pour construire une valeur de ce type, on doit fournir toutes les composantes simultanément.

Si un type $A$ a 3 habitants possibles et un type $B$ en a 5, alors le type $(A, B)$ en a exactement 15, soit $3 \times 5$. C’est le produit cartésien au sens ensembliste : chaque combinaison possible de valeurs constitue un habitant distinct du type produit.

Les types sommes

Les sum types, qui sont ici les unions discriminées, les variants ou les enums, incarnent au contraire la disjonction exclusive . Une valeur d’un sum type est exactement une des alternatives possibles, jamais plusieurs.

Si $A$ a 3 habitants et $B$ en a 5, alors $A | B$ en a 8, soit $3 + 5$. On additionne les possibilités plutôt que de les multiplier.

Cette distinction n’est pas qu’un exercice mathématique abstrait : elle guide directement nos choix de modélisation en nous forçant à expliciter si deux informations coexistent nécessairement ou s’excluent mutuellement.

Chaque combinaison invalide autorisée par un type est un bug potentiel. Un type « statut de commande » qui permet 100 combinaisons alors que 5 seulement ont un sens métier contient 95 chemins vers des comportements incorrects : autant d’occasions de facturer un client pour une commande jamais expédiée, ou d’envoyer un colis sans avoir débité le paiement.

Éliminer les états invalides

Cette algèbre explique pourquoi les sum types sont si puissants pour éliminer les états invalides.

Considérons une entité qui peut être soit en état « brouillon » avec un contenu modifiable, soit en état « publié » avec une date de publication :

• Un product type naïf { status: Status, content: string, publishedAt?: Date } autorise $2 \times \infty \times (\infty + 1)$ combinaisons, incluant des aberrations comme un brouillon avec une date de publication.
• Un sum type Draft { content } | Published { content, publishedAt } réduit drastiquement l’espace des états en n’autorisant que les combinaisons sémantiquement valides.

On passe d’un produit cartésien pollué à une somme précise. Cette réduction a une conséquence directe sur les coûts de test : moins d’états possibles signifie moins de cas à vérifier, moins de branches if (status === X && field !== null) dispersées dans le code, et moins de temps passé à diagnostiquer des bugs liés à des états « impossibles » qui se produisent quand même.

En pratique avec TypeScript

TypeScript illustre bien cette dualité avec ses interfaces (produits) et ses unions discriminées (sommes).

Un pattern courant consiste à utiliser un champ discriminant, souvent nommé type ou kind, pour transformer ce qui serait autrement une union structurelle ambiguë en une somme explicite. Le compilateur peut alors effectuer du narrowing : dans chaque branche d’un switch sur le discriminant, il sait exactement quelle variante est active et quels champs sont disponibles.

C’est l’exploitation directe de la sémantique OU : à un instant donné, on est dans une branche, pas dans plusieurs.

Les types unitaire et impossible

Cette perspective algébrique nous donne également un vocabulaire pour raisonner sur les types unitaire et impossible :

• Le type void ou unit (un seul habitant) est le neutre de la multiplication : $A \times \text{unit} \cong A$
• Le type never (zéro habitants) est le neutre de l’addition : $A \mid \text{never} \cong A$
• Et l’absorbant de la multiplication : $A \times \text{never} \cong \text{never}$

Ces identités ne sont pas des curiosités théoriques : elles expliquent pourquoi une fonction retournant never prouve qu’un cas est impossible, ou pourquoi un champ de type never rend tout le record inhabité.

Maîtriser cette algèbre, c’est disposer d’un outil mental pour concevoir des types qui expriment exactement ce qu’on veut autoriser, ni plus ni moins.