Refinement Types et Dependent Types : vers des types qui prouvent

Au-delà du typage classique, certains systèmes permettent d’encoder des propriétés plus fines. Le compilateur devient alors un assistant de preuve, et permet de forcer des invariants métiers encore plus précis.

Les refinement types

Les refinement types constituent une extension des systèmes de types traditionnels où l’on raffine un type de base par un prédicat logique.

Plutôt que de simplement déclarer qu’une variable est un entier, on peut spécifier qu’elle est, par exemple :

• Un entier strictement positif
• Un entier compris entre 0 et 100
• Un entier pair

La notation classique emprunte à la théorie des ensembles : $\{ x : \text{Int} \mid x > 0 \}$ désigne le type des entiers satisfaisant le prédicat $x > 0$.

Le compilateur ou un solveur externe (souvent un SMT solver) vérifie alors statiquement que toute valeur affectée à ce type respecte la contrainte, transformant des erreurs runtime en erreurs de compilation.

Les dependent types

Les dependent types vont plus loin encore : ils permettent aux types de dépendre de valeurs.

Dans un système à types dépendants, on peut exprimer le type $\text{Vector}\langle n \rangle$ où $n$ est une valeur entière représentant la longueur du vecteur. La fonction :

$\text{concat} : \text{Vector}\langle n \rangle \to \text{Vector}\langle m \rangle \to \text{Vector}\langle n + m \rangle$

encode dans sa signature que la concaténation produit un vecteur dont la longueur est la somme des longueurs des opérandes.

Le type $\text{head} : \text{Vector}\langle n + 1 \rangle \to A$ garantit qu’on ne peut appeler cette fonction que sur un vecteur non vide : le cas d’erreur disparaît par construction.

Les types deviennent un langage de spécification formelle vérifié par le compilateur.

Refinement vs Dependent : quelle différence ?

La distinction entre ces deux approches est parfois floue, mais on peut la résumer ainsi :

• Les refinement types enrichissent des types existants par des prédicats vérifiés séparément, souvent par un solveur automatique
• Les dependent types intègrent les valeurs directement dans le système de types lui-même, requérant parfois des preuves explicites

Liquid Haskell  illustre l’approche refinement : on annote du code Haskell standard et un solveur SMT vérifie les contraintes. Idris , Agda  ou Lean  incarnent l’approche dépendante pure : les preuves font partie intégrante du programme et le développeur doit parfois les construire manuellement.

Applications pratiques

En pratique, ces systèmes permettent d’encoder des invariants impossibles à exprimer dans des langages comme TypeScript ou Java :

• L’accès à un tableau peut être prouvé bounds-safe par le type lui-même
• Une fonction de division peut exiger un dénominateur de type $\{ x : \text{Int} \mid x \neq 0 \}$, éliminant toute possibilité de division par zéro
• Un protocole réseau peut être modélisé comme une machine à état au niveau des types, rendant impossible l’envoi d’un message dans le mauvais ordre

On dépasse le simple Make Illegal States Unrepresentable pour atteindre « Make Illegal Operations Untypeable » : les programmes qui compilent sont corrects par construction, du moins vis-à-vis des propriétés encodées.

Limites et compromis

Cependant, cette puissance a un coût :

• L’inférence de types devient souvent indécidable ou exige des annotations lourdes
• Les messages d’erreur peuvent être cryptiques, mêlant logique formelle et contraintes de solveur
• L’écosystème est plus restreint : moins de bibliothèques, moins de tooling, courbe d’apprentissage abrupte
• Le temps passé à convaincre le compilateur peut dépasser le temps passé à écrire la logique elle-même

Ces outils trouvent leur place dans les domaines où la correction est critique (systèmes embarqués, cryptographie, protocoles de consensus, etc.) mais restent marginaux dans le développement applicatif courant.

Ils représentent néanmoins l’horizon vers lequel les systèmes de types progressent graduellement, et des fragments de leurs idées infusent peu à peu dans les langages mainstream.