Les kinds : le garde-fou invisible

Un type range tes valeurs : 3 est un nombre, up est un statut. Mais tous les types ne se valent pas. Sur un nombre, tu peux calculer ; sur un statut, ça n'a aucun sens. Cette distinction — ce qu'on a le droit de faire d'un type — c'est le kind.

Le point essentiel : tu ne t'en occupes pas. Le kind est inféré, jamais déclaré — il n'y a pas de déclaration kind à écrire, pas de taxonomie à maintenir. Fix classe chaque type d'après sa forme et son usage, et s'en sert pour attraper tes fautes avant la moindre exécution. C'est un garde-fou : tu ne le vois que le jour où il te sauve.

Ce que Fix infère

Une poignée de classes suffit — tu les croiseras dans les messages d'erreur, pas dans ton code :

Kind	Le type est…	Inféré de
`number`	calculable (additionner, comparer)	valeurs numériques, usage dans `add`/`<`
`enum`	un choix parmi des valeurs nommées	`type t = a \| b \| c.`
`record`	un assemblage de champs	un constructeur à plusieurs champs
`adt`	les deux à la fois	`type` mixte (choix de formes, chacune avec champs)
`numeric_record`	un assemblage et calculable	structure à champs numériques

Tu reconnais l'algèbre des types derrière : un enum est une somme (« l'un OU l'autre »), un record est un produit (« ceci ET cela »), un adt combine les deux. Le kind, c'est cette forme, nommée par ce qu'elle autorise.

Le garde-fou en action

Tu n'écris que des types et des signatures — jamais un kind :

type pays = fr | de | it.
sig(zone, [pays]).
zone(fr).

Maintenant la faute : un calcul sur un pays.

plus_un(X) :- zone(Z), add(Z, 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

Refusé à la compilation. Tu n'as déclaré nulle part que pays n'est pas calculable — Fix l'a inféré de la forme du type (des valeurs nommées → un choix, pas un nombre), et a fait le rapprochement seul : add exige du number, pays n'en est pas, refus.

C'est la division du travail entre les deux garde-fous :

la faute dans une donnée (une valeur hors du type) est attrapée par le type : fait mal typé, avec la position fautive et la correction proposée dans le message ;
la faute dans une opération (un calcul sur l'incalculable) est attrapée par le kind : règle mal typée, avec la position et la forme de valeur en cause (« une étiquette là où… attend un nombre »).

Interrogeable quand même

Invisible ne veut pas dire inaccessible. Déclarer un type peuple la relation kind_of/2, que tu peux interroger comme n'importe quelle autre :

?- kind_of(statut, K).
K = enum

kind_of est la surface observable des kinds — le pendant L₂ de has_type. Observable, mais pas programmable : une règle de tête kind_of est inerte pour le kindage (le kind d'un type vient de sa déclaration, jamais d'une règle — c'était un trou de soundness, la voie a été retirée). Le détail : TLLP.

Pas une couche en plus

Le réflexe serait d'imaginer un « système de kinds » à côté du langage. Il n'y en a pas : classer un type est déjà du calcul relationnel, fait par le même moteur que tout le reste. La différence avec les types, c'est seulement que ce calcul-là ne te demande rien — pas une annotation, pas une déclaration.

C'est le refrain de Fix, poussé un cran plus loin : les types ont des kinds non pas parce qu'on a ajouté une théorie, mais parce que le moteur qui résout tes règles sait aussi classer tes types — silencieusement.

Les bords honnêtes

Le kind résume les opérations qu'un type supporte, pas une propriété arbitraire. Ce n'est pas un langage de contraintes général.
La liste des kinds est volontairement courte : elle nomme des intentions d'usage, pas une taxonomie exhaustive.
kind_of ne répond que pour les types déclarés (par type) : le kind d'un type purement inféré travaille en interne sans être matérialisé en fait.

À côté

Les types comme programme (TLLP) — et pourquoi le garde-fou, lui, ne se programme pas.
Apprendre — 2. Les types — la première rencontre.
Lire un refus — les deux messages du garde-fou, en contexte.