Le paramétrage des types

Dans Fix, un type est un terme. Et comme tout terme, il peut prendre des arguments : on le paramètre. Cette seule idée couvre ce que d'autres langages séparent en deux — les génériques d'un côté, les types dépendants de l'autre.

Un type prend des arguments

type couleur = rouge | vert | bleu.
type list(T) = nil | cons(T, list(T)).

list(T) n'est pas un type — c'est une famille. T est un paramètre (une variable de type, en MAJUSCULE) : une liste de n'importe quoi.

L'instancier

On choisit t dans une signature, et le paramètre se propage — chaque élément est vérifié comme un t :

sig(pile, [list(couleur)]).
sig(nombres, [list(number)]).

pile(cons(rouge, cons(vert, nil))).
nombres(cons(1, cons(2, nil))).

Le même list(T) sert deux types. Glisse un intrus — mauve n'est pas une couleur — et Fix refuse au chargement :

pile(cons(rouge, cons(mauve, nil))).

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

Plusieurs paramètres

type pair(A, B) = pair(A, B).
sig(cellule, [pair(couleur, number)]).

cellule(pair(rouge, 7)).

Deux paramètres, A et B, fixés à l'instanciation. Inverse-les :

cellule(pair(7, rouge)).

fix: fait mal typé : `cellule(pair(7, rouge))`
    position 0 : `pair(7, rouge)` n'est pas une valeur du type `pair(couleur,number)`.
    Corrige : ajoute cette valeur au type, ou utilise une valeur déjà déclarée du type.
    → :help types

Les types dépendants en découlent

Rien n'oblige un argument de type à être un type. Puisqu'un type est un terme, un argument peut être une valeur :

has_type(m, vec(int, 3)).
has_type(n, vec(couleur, 3)).

Le 3 est une valeur : c'est un type dépendant — et ce n'est pas une feature de plus, il découle du paramétrage. vec(couleur, 3) mélange même les deux : couleur est un type (paramétrique), 3 une valeur (dépendant). On l'interroge comme tout le reste :

?- has_type(X, vec(couleur, 3)).
X = n

La page types dépendants déroule le cas où le moteur calcule l'indice.

Pourquoi ça marche : un type est un terme

Tout tient à ça. Un type est un terme composé ; ses arguments sont des termes — des types ou des valeurs, sans distinction de nature. Et ce qui vérifie tout, c'est le même moteur : has_type calculé par les règles (TLLP), où la propagation du paramètre est l'unification.

Fix n'a rien ajouté ni pour les génériques ni pour les dépendants. Les deux tombent du fait qu'il résout des termes.

Ce que la casse dit — les trois phrases

• Pour tout type A, paire(A) est le type des p(x, y) où x et y sont tous deux du type A.
• w accepte une paire(T) pour un certain type T — chaque fait choisit son T, et le tient d'un bout à l'autre du fait.
• paire(animal) est le type des paires d'animaux. Un nom en minuscule désigne toujours un type précis — jamais « n'importe lequel ».

Le contraste en une ligne : une lettre de casse porte toute la différence, et l'AST la porte avant elle.

Les bords honnêtes

• Le paramètre-type est une variable, en MAJUSCULE (list(T)) ; il se lie au moment de l'instanciation, dans la signature. Une minuscule (list(t)) désigne LE type nommé t — jamais « n'importe lequel ».
• Un type paramétré non instancié (list(T), T libre) décrit la forme ; c'est la signature qui fixe T pour typer des faits.

À côté

• Les types dépendants (RDT) — le paramétrage par une valeur, calculée par le moteur.
• Les types comme programme (TLLP) — le moteur qui vérifie, en règles.
• Les kinds — au-dessus des types.