Re: Typage structurel

Mais comment on prouve au type checker que l'opérateur + que l'on définit est bien commutatif ?
Dans les faits, elle ressemble à quoi la syntaxe pour ce genre de propriété ?

En coq, cela pourrait ressembler à ça:

Theorem plus_est_commutatif: forall a, b. a + b = b + a.
Proof. Admitted.

;) Mais je pense amicalement que tu me provoques un peu sachant que tu sais cela très bien.

Plus sérieusement,

On se contente de l'affirmer sans preuve ?

Oui. En Haskell, chaque "class" (qui est ce qui se rapproche le plus des concepts du C++) vient souvent avec des "lois" qu'un utilisateur peut s'attendre à voir pris en compte par tout type de la class. Par exemple map f (map g l) doit être la même chose que map (f.g) l. Appliquer g puis f sur un chaque élément de "la collection" l doit renvoyer la même chose qu'appliquer la composition de f et g (f.g) sur chaque élément de l.

Mais le langage ne le vérifie absolument pas. C'est laissé à la charge du développeur d'être cohérent et de s'assurer du respect des lois. Il existe des outils de tests qui peuvent tenter de prouver les propriétés, soit avec un solveur type z3, soit par génération de valeur aléatoires.

Mais alors, cela apporte quoi de plus ?

C'est juste un problème d'interface ou de contrat que tu passes avec ton développeur et la libraire. Si on reprend l'exemple de la commutativité, si en tant que développeur je sais que le type générique (e.g. template) que j'utilise est commutatif pour mon opération, alors je peux me permettre certaines choses. On peut me mentir, mais au moins j'aurais prévenu. Inversement, en demandant que le type en entrée soit commutatif, je préviens l'utilisateur et il ne peut pas rater la contrainte que je lui demande.