Les types comme programme : TLLP

Dans la plupart des langages, le système de types est une boîte noire. Quelqu'un l'a écrit une fois, il vérifie ton code, et tu le subis. Tu ne peux pas lui ajouter une règle.

En Fix, les types ne sont pas des annotations passives : ce sont des relations, exactement comme tes faits. Et sur une relation, tu sais déjà faire une chose — écrire des règles.

C'est ça, TLLP (Type-Level Logic Programming) : des règles d'inférence dont la tête est un type.

Trois niveaux, un seul moteur

Tu connais déjà has_type(X, T) — « le terme X a le type T ». Et kind_of(T, K) — « le type T a le kind K ». Trois niveaux, une seule base de faits :

TLLP : des types affinés, par règle

Voici la vraie force. Tu n'es pas limité aux types que tu déclares : tu peux en définir de nouveaux par une règle, en fonction de ce que tes données contiennent.

% un "utilisateur complet" n'est pas déclaré : il se DÉDUIT
has_type(U, utilisateur_complet) :-
    has_type(U, utilisateur),
    a_email(U),
    a_role(U).

« Un utilisateur complet, c'est un utilisateur qui a un e-mail et un rôle. » Tu viens d'écrire un type affiné — une contrainte métier — comme une règle de typage. Le moteur range chaque utilisateur dans utilisateur_complet ou non, et le compilateur peut s'en servir pour accepter ou refuser la suite.

Aucun langage de contraintes à côté (pas d'OCL, pas de validateur séparé) : la contrainte est une règle de type, dans le même fichier, vérifiée par le même moteur.

Et les kinds ? Observables, pas programmables

L'étage L₂ s'interroge (?- kind_of(statut, K). → K = enum), mais ne se programme pas : le kind d'un type vient de sa déclaration (type … = …) et de l'inférence, jamais d'une règle. Une clause de tête kind_of plate compile et s'évalue comme un prédicat ordinaire, mais elle est inerte pour le kindage — elle n'élargit ni ne modifie le kind d'aucun type.

Ce n'est pas une lacune, c'est un retrait délibéré : la voie « KLLP programmable » laissait une règle élargir un enum et y glisser un nombre — un trou de soundness. Le kind est un garde-fou ; un garde-fou que l'utilisateur peut reprogrammer n'en est plus un.

Trois niveaux, toutes les directions

Le même moteur fait circuler l'information dans les trois sens :

• Horizontal — l'inférence complète sur les valeurs (Datalog) et sur les types (TLLP).
• Montant — de bas en haut : le type se déduit des valeurs, le kind se déduit du type. Tu calcules le typage au lieu de le déclarer.
• Descendant — de haut en bas : les types portent des valeurs comme indices. C'est le sujet des types dépendants.

Une seule passe les croise tous.

Pourquoi ça change tout

Le système de types n'est plus une chose qu'on subit, c'est une chose qu'on programme :

• tu étends le typage avec tes propres règles, sans toucher au moteur ;
• tes invariants métier deviennent des types affinés, pas des commentaires ;
• et c'est sound — Fix garantit que ce qui est dérivé reste bien typé (préservation + progression, à la Wright-Felleisen).

C'est la même idée que partout en Fix : pas une extension bolt-on, mais le même geste — écrire des règles — appliqué un cran plus haut. Avec une exception assumée : le kind, garde-fou du système, reste hors de portée des règles.

Les bords honnêtes

• Le TLLP reste du raisonnement à la Datalog : ça termine, c'est stratifié. Ce n'est pas de la théorie des types dépendante complète, et ça ne cherche pas à l'être.
• Les règles de type obéissent aux mêmes contraintes que les autres (stratification, agrégats idempotents en récursion, garde de terminaison — une tête has_type qui construit un terme est refusée, voir La terminaison).
• kind_of : interrogation pleine ; règles plates inertes pour le kindage ; règles récursives refusées par la garde.

À côté

• Les kinds — pourquoi le garde-fou n'est pas programmable.
• Les types dépendants (RDT) — la direction descendante.
• Référence : règles de types — la forme exacte.
• Apprendre — 2. Les types — la première rencontre.