La Correspondance de Curry-Howard : lien entre programmes et preuves

La correspondance de Curry-Howard, parfois appelée isomorphisme de Curry-Howard, établit une équivalence profonde entre deux domaines apparemment distincts : la logique formelle et la théorie des types. Le terme isomorphisme signifie ici que ces deux domaines ont exactement la même structure : ce sont deux façons de regarder la même chose.

L’isomorphisme fondateur

Découverte indépendamment par Haskell Curry dans les années 1930 et William Alvin Howard en 1969, cette correspondance révèle que les types sont des propositions logiques et les programmes sont des preuves de ces propositions.

Un programme qui compile est donc littéralement une démonstration que son type est habité, c’est-à-dire qu’il existe au moins une valeur satisfaisant cette spécification. Cette dualité n’est pas une simple analogie poétique ; c’est une identité structurelle rigoureuse.

Les correspondances entre types et propositions logiques

Les correspondances élémentaires entre types d’une part et propositions logiques d’autre part sont élégantes dans leur simplicité :

Cette similitude de structure, qui apparait clairement dans le tableau, est ce qui constitue l’isomorphisme¹ en lui-même.

Voir aussi : Algèbre des types : produits et sommes

Le type never et la contradiction

Cette correspondance éclaire le rôle du type never en TypeScript ou Nothing en Scala.

Une fonction de type $A \to \text{never}$ affirme « si A est vrai, alors il y a contradiction » : autrement dit, A est faux, A est inhabité (= A ne contient pas de valeur). C’est exactement le principe de ex falso quodlibet : du faux, on peut dériver n’importe quoi.

Quand le compilateur infère que le type d’une expression est never, il prouve ainsi que ce chemin d’exécution est impossible. Les analyses d’exhaustivité des pattern matching (exhaustive pattern matching) exploitent ce mécanisme : si tous les cas sont couverts, le cas résiduel est de type never, prouvant qu’aucun cas n’a été oublié.

Types polymorphes et quantificateurs

Les types polymorphes² correspondent aux quantificateurs de la logique.

Le quantificateur universel $\forall$, qui se prononce « pour tout » : une fonction de type $\forall A. A \to A$ (qui signifie « pour tout type A, une fonction de A vers A ») doit fonctionner pour n’importe quel type A.

function identity<A>(x: A): A {
  return x  // seule implémentation possible
}

from typing import TypeVar
 
A = TypeVar('A')
 
def identity(x: A) -> A:
    return x  # seule implémentation possible

public static <A> A identity(A x) {
    return x;  // seule implémentation possible
}

identity :: a -> a
identity x = x  -- seule implémentation possible

Cette fonction ne peut pas inspecter ce qu’est A, ni faire de cas particulier : c’est l’appelant qui choisit. Le type contraint l’implémentation au point de la déterminer entièrement.

Le quantificateur existentiel $\exists$, qui se prononce « il existe » : un type comme $\exists A. (A, A \to \text{String})$ signifie « il existe un type A, et je fournis une valeur de ce type plus une fonction pour la convertir ».

interface Showable {
  // A est caché - l'appelant ne sait pas ce que c'est
  show: () => string
}
 
const myShowable: Showable = {
  // l'implémenteur choisit A = number
  show: () => String(42)
}

from typing import Protocol
 
class Showable(Protocol):
    # A est caché - l'appelant ne sait pas ce que c'est
    def show(self) -> str: ...
 
class MyShowable:
    # l'implémenteur choisit A = int
    def __init__(self):
        self._value = 42
 
    def show(self) -> str:
        return str(self._value)

interface Showable {
    // A est caché - l'appelant ne sait pas ce que c'est
    String show();
}
 
Showable myShowable = new Showable() {
    // l'implémenteur choisit A = Integer
    private final int value = 42;
 
    public String show() {
        return String.valueOf(value);
    }
};

-- Type existentiel avec GADT
data Showable where
  MkShowable :: Show a => a -> Showable
 
-- l'implémenteur choisit a = Int
myShowable :: Showable
myShowable = MkShowable (42 :: Int)
 
showIt :: Showable -> String
showIt (MkShowable x) = show x

Ici c’est l’implémenteur qui choisit A, et l’appelant ne sait pas ce que c’est : c’est le fondement des types abstraits et de l’encapsulation.

Cette correspondance s’étend aux logiques d’ordre supérieur avec les dependent types : un type comme $\forall n : \text{Nat}. \text{Vector}\langle n \rangle \to \text{Vector}\langle n \rangle$, qui se lit « pour tout entier naturel n, une fonction d’un vecteur de taille n vers un vecteur de taille n », exprime une proposition quantifiant sur les valeurs, pas seulement sur les types.

Les assistants de preuve comme Coq , Agda  ou Lean  exploitent pleinement cette équivalence : on y écrit des programmes qui sont des preuves de théorèmes mathématiques.

Implications pratiques dans la programmation au quotidien

La correspondance de Curry-Howard semble très théorique et abstraite, mais les implications pratiques pour le développeur au quotidien sont réelles :

• Concevoir une signature de fonction, c’est énoncer un théorème
• Implémenter cette fonction, c’est le démontrer
• Un type trop faible (comme any) correspond à une proposition triviale qui n’affirme rien d’intéressant
• Un type impossible à implémenter révèle une spécification contradictoire

Concrètement, pour un développeur TypeScript ou Python : quand le compilateur refuse votre code avec une erreur de type, il vous dit que votre « preuve » est invalide. Et quand vous choisissez unknown plutôt que any, vous vous engagez à prouver que vous avez correctement identifié le type avant de l’utiliser.

Les théorèmes libres  (free theorems) de Wadler montrent que certains types polymorphes n’ont qu’une seule implémentation possible : le type est la spécification complète.

La correspondance de Curry-Howard nous invite ainsi à voir le typage non comme une contrainte bureaucratique, mais comme un système de raisonnement formel où chaque programme qui compile constitue une preuve vérifiée mécaniquement. C’est, en quelque sorte, le poka-yoke  du développeur : un mécanisme qui rend certaines erreurs structurellement - mathématiquement, en réalité - impossibles.