Apprendre Fix — 2. Les types

Deuxième étape. À la première tu as posé le typage — fermé un statut, vu un intrus refusé à la compilation. Ici tu en fais un métier concret : fermer tes vocabulaires métier, laisser le kind te garder sans rien écrire, structurer avec des ADT (list(T)). À chaque étage, une faute de plus attrapée à la compilation. Et tout au bout, si tu en as besoin, deux capacités plus avancées — un type qui se définit par une règle, un type qui porte une valeur calculée. Compte 30 minutes.

1. Fermer un jeu de valeurs

Tu as déjà fermé le statut à l'étape 1 — reprenons-le posément, il y a plus à en dire. L'état d'un service ne peut être que l'un de trois :

% l'état d'un service : trois valeurs, pas une de plus
type statut = up | degrade | down.
sig(etat, [service, statut]).

etat(web, up).
etat(api, degrade).
etat(db, up).

Deux déclarations : type ferme statut (seuls up, degrade, down sont admis), et sig dit ce que etat attend à chaque position. Quant à service, tu ne le déclares nulle part : un nom de type sans déclaration reste ouvert — n'importe quel nom de service passe, on ne veut pas les lister d'avance.

Maintenant, la faute de frappe :

etat(auth, retabli).

$ fix services.fix
fix: fait mal typé : `etat(auth, retabli)`
    position 1 : `retabli` n'est pas une valeur du type `statut`.
    Corrige : ajoute cette valeur au type, ou utilise une valeur déjà déclarée du type.
    → :help types

Refusé à la compilation — le programme ne se charge même pas, et le message fait le diagnostic à ta place : le fait fautif, la position, et la correction à envisager. Il n'y a rien à activer : le typage fort est le défaut, non débrayable. La faute est morte avant la production.

Note ce que tu n'as pas fait : annoter tes faits. Un sig par prédicat suffit, Fix vérifie tout le reste tout seul — et un programme sans aucune signature reste accepté tel quel (le Datalog nu de l'étape 1 tournait déjà). Tu choisis où tu fermes.

2. Le kind : le garde-fou que tu ne déclares jamais

Un cran au-dessus du type, il y a ce qu'on peut en faire : calculer, ou pas. C'est le kind — et tu ne t'en occupes pas : il est inféré, jamais déclaré. Continue d'écrire tes signatures, rien d'autre :

sig(latence, [service, ms]).
latence(db, 20).

double(S, T) :- latence(S, L), add(L, L, T).

?- double(db, T).
T = 40

ms n'est déclaré nulle part — Fix a inféré de l'usage que c'est un nombre, et le calcul passe. Maintenant la faute : additionne un statut :

plus_grave(S, X) :- etat(S, E), add(E, 1, X).

fix: règle mal typée : `add` — à la position 1 de `add`, une règle produit une étiquette là où le type déclaré attend un nombre
    → :help types

Tu n'as jamais dit que statut n'est pas calculable : Fix l'a inféré de sa forme (des valeurs nommées → un choix, pas un nombre) et refuse le calcul à la compilation. C'est ça, le kind : un garde-fou invisible qui travaille sans une ligne de toi. Le tour complet : Les kinds.

3. Structurer : l'ADT

Les valeurs composées se déclarent pareil — avec des paramètres en MAJUSCULE (un paramètre de type est une variable ; une minuscule désigne un type nommé) :

type couleur = rouge | vert | bleu.
type list(T) = nil | cons(T, list(T)).
sig(stock, [list(couleur)]).

stock(cons(rouge, cons(vert, nil))).

?- stock(L).
L = cons(rouge, cons(vert, nil))

Glisse un intrus au fond de la liste — cons(rouge, cons(7, nil)) :

fix: fait mal typé : `stock(cons(rouge, cons(7, nil)))` ne respecte pas la signature de `stock`.
    → :help types

La vérification descend dans la structure, quelle que soit la profondeur.

4. Le type qui se programme

Un cran plus loin — plus avancé, à garder pour quand tu en as besoin. has_type/2 — « X a le type T » — est un prédicat ordinaire. Donc tu peux écrire des règles dessus, comme sur impacte. Définis un type que personne n'a déclaré :

% un service critique n'est pas déclaré : il se DÉDUIT
has_type(S, critique) :- latence(S, L), L > 30.

?- has_type(S, critique).
S = api

Tu viens d'écrire un type affiné : une contrainte métier, exprimée comme une règle de typage, calculée par le même moteur que tout le reste. Pas de langage de contraintes à côté. C'est le TLLP — Les types comme programme.

5. Le type qui calcule

Dernier cran, avancé lui aussi. Un type peut porter une valeur — et cette valeur se calcule. Tes bases de données tournent en grappes :

has_type(grappe_a, cluster(db, 2)).
has_type(grappe_b, cluster(db, 3)).
has_type(grappe_c, cluster(auth, 1)).

% fusionner deux grappes DU MÊME service : les tailles s'additionnent
fusion(A, B, cluster(S, N)) :-
    has_type(A, cluster(S, M)),
    has_type(B, cluster(S, K)),
    add(M, K, N).

?- fusion(grappe_a, grappe_b, T).
T = cluster(db, 5)

?- fusion(grappe_a, grappe_c, T).
false.

Deux choses viennent de se passer. La taille du résultat (5) a été calculée par le type. Et la fusion inter-services n'a pas de solution : le S partagé entre les deux prémisses l'interdit — la contrainte est dans la structure, pas dans un test que tu aurais pu oublier. Ajoute les tests :

test(fusion_meme_service, holds)      :- fusion(grappe_a, grappe_b, cluster(db, 5)).
test(fusion_services_differents, fails) :- fusion(grappe_a, grappe_c, T).

$ fix --test services.fix
...
1 suite(s) · 2 passé(s) · 0 échoué(s)

Un détail de forme qui compte : le type dérivé vit dans son prédicat (fusion/3), et les objets sont nommés (grappe_a) — construire un terme neuf en tête d'une règle récursive serait refusé par la garde de terminaison (étape 1, le pourquoi). Les exemples complets — matrices, unités, typestate : Les types dépendants.

Ce que tu sais faire

Fermer un jeu de valeurs (type + sig), laisser le kind te garder (inféré, tu n'écris rien), structurer (list(T)), définir un type par une règle (TLLP), et faire calculer un type (RDT) — avec, à chaque étage, la faute attrapée à la compilation.

→ 3. Interroger : voir ce qui manque (la négation) et résumer (les agrégats) — puis les modules, la syntaxe, et dériver.