Comment les types se prouvent — le système de types de TypeScript et la correspondance de Curry–Howard

Résumé :

• Cet article propose de considérer le système de types de TypeScript non comme un simple vérificateur de types statique, mais comme un système de preuve issu de la logique.
• En s’appuyant sur la correspondance de Curry–Howard (Type = Proposition, Program = Proof), il explique conceptuellement pourquoi l’inférence de types est possible.
• Il met en relation des fonctionnalités de TypeScript comme les types de fonction, les génériques, les types conditionnels et le rétrécissement de type avec l’implication logique, la quantification universelle et l’analyse par cas.
• Il interprète le processus de vérification de types non comme une application de règles, mais comme une validation des relations entre propositions.
• L’accent est mis moins sur les détails d’implémentation que sur le contexte de conception et la structure mathématique du système de types de TypeScript.

Résumé détaillé :

1. Contexte : pourquoi l’inférence de types est-elle possible ?
   Dans les langages à typage statique, l’inférence de types est souvent expliquée comme un problème d’implémentation : « comment le compilateur parvient-il à faire correspondre les types ? ».
   Cet article prend une étape de recul et s’interroge sur la raison fondamentale qui rend l’inférence de types possible en premier lieu.
   Il propose comme réponse une lecture du système de types comme système de preuve en logique.

2. Fondement théorique : la correspondance de Curry–Howard
   Selon la correspondance de Curry–Howard, un type (Type) correspond à une proposition (Proposition) et un programme (Program) à une preuve (Proof) de cette proposition.
   Dans cette perspective, le typage est interprété comme le processus qui vérifie si un programme satisfait une proposition donnée.

3. Correspondance entre les fonctionnalités de TypeScript et les structures logiques
   L’article relie les principales fonctionnalités de TypeScript de la manière suivante :

• type de fonction → implication logique (Implication)
• génériques → quantification universelle (Universal Quantification)
• types conditionnels / rétrécissement de type → analyse par cas (Case Analysis)
  Cela permet d’expliquer pourquoi certaines expressions de type paraissent naturelles,
  et pourquoi d’autres types sont structurellement difficiles à exprimer.

4. Limites du système de types et choix de conception
   Dans cette optique, les contraintes et limites de TypeScript ne relèvent pas d’un « manque de fonctionnalités », mais de choix de conception destinés à préserver la cohérence logique.
   L’article se concentre moins sur des techniques ou astuces pratiques que sur la philosophie et les fondements mathématiques qui ont façonné le système de types.