Fonctions totales et partielles : la promesse du type

Une fonction totale est une fonction qui termine et produit une valeur valide pour toute entrée de son domaine déclaré.

La promesse de la signature

Si une fonction a pour signature $f : A \to B$, la totalité garantit que pour chaque habitant de $A$, on obtiendra un habitant de $B$ : sans exception, sans boucle infinie (la fonction ne terminant jamais), sans crash (la fonction mentant, en quelque sorte).

Une fonction partielle, en revanche, ne tient cette promesse que pour un sous-ensemble de son domaine : elle peut diverger, lever une exception, ou retourner null pour certaines entrées.

La distinction semble académique, mais elle touche au cœur de ce que signifie la confiance qu’on accorde à une signature de type.

Les fonctions partielles déguisées

Les fonctions partielles sont omniprésentes dans la programmation quotidienne, souvent déguisées en fonctions totales :

• $\text{head} : \text{List}\langle A \rangle \to A$ ment sur son type : elle échoue sur la liste vide
• $\text{parseInt} : \text{string} \to \text{number}$ promet un nombre mais peut retourner NaN ou lever une exception
• dict.get(key) suggère qu’on obtiendra une valeur, mais que se passe-t-il si la clé est absente ?

Ces fonctions violent le contrat implicite de leur signature : le type prétend couvrir tous les cas, mais l’implémentation en exclut certains.

Le développeur doit savoir quels cas sont problématiques et les gérer : une connaissance qui n’est pas encodée dans le système de types. Cette connaissance ajoute à la charge mentale, et rend le programme plus fragile.

Rendre une fonction totale

Rendre une fonction partielle totale consiste à faire correspondre son type à son comportement réel. Deux stratégies principales s’offrent à nous :

1. Restreindre le domaine : plutôt que $\text{head} : \text{List}\langle A \rangle \to A$, on écrit $\text{head} : \text{NonEmptyList}\langle A \rangle \to A$, déplaçant la responsabilité de la preuve vers l’appelant.

2. Élargir le codomaine : $\text{head} : \text{List}\langle A \rangle \to \text{Option}\langle A \rangle$ admet explicitement la possibilité d’absence.

Dans les deux cas, le type devient honnête : il promet exactement ce qu’il peut tenir.

L’article Parse, Don’t Validate d’Alexis King privilégie la première approche ; les langages fonctionnels traditionnels emploient souvent la seconde via Option ou Either. Chez evryg, nous parlons plutôt de « contraindre en amont » (au niveau du type des arguments de la fonction - le domaine) ou « d’élargir en aval » (au niveau du type de retour - le codomaine).

La dimension logique : Curry-Howard

Du point de vue de Curry-Howard, cette distinction entre fonction totale et fonction partielle prend une dimension logique.

• Une fonction totale $A \to B$ constitue une preuve constructive que « $A$ implique $B$ » : pour toute preuve de $A$, on peut construire une preuve de $B$. Cette preuve se construit par l’existence même de la fonction, correctement implémentée.
• Une fonction partielle ne prouve rien de tel : elle affirme seulement que parfois, de certains $A$, on peut obtenir un $B$. Le reste du temps, cette fonction ment.

Les assistants de preuve comme Coq  ou Agda  exigent la totalité par défaut, car une fonction non terminante permettrait de « prouver » n’importe quoi, y compris des contradictions.

Le termination checker vérifie que chaque récursion progresse vers un cas de base, garantissant que la preuve-programme s’achève toujours.

Vers la totalité en pratique

En pratique, la totalité absolue est un idéal rarement atteint dans les langages mainstream. Les sources de partialité sont nombreuses :

• Effets de bord
• Exceptions
• Timeouts réseau
• Épuisement mémoire

Ces cas échappent aux types conventionnels.

Cependant, tendre vers la totalité améliore considérablement la robustesse du code. Chaque fonction partielle convertie en fonction totale est un piège de moins pour le développeur futur, et une alerte à 3h du matin évitée.

Les exceptions inattendues en production ont un coût humain : astreintes, burnout, turnover. Les meilleurs ingénieurs partent quand ils passent plus de temps à éteindre des incendies qu’à construire. Des fonctions totales signifient moins de surprises, une astreinte plus sereine, et une équipe qui reste.

Les types deviennent des contrats fiables plutôt que des approximations optimistes. Le compilateur, armé de types honnêtes, peut enfin remplir son rôle de vérificateur: non pas de la simple syntaxe, mais bien des propriétés sémantiques du programme exprimées sous forme de types statiques.