kantien a écrit 1187 commentaires

Aucune idée, je ne suis qu'utilisateur et non développeur Debian. Je ne suis pas de près ce qui se passe au sein du projet.

Sinon Mehdi (ça y est, j'ai bien écrit son prénom ! \o/) n'a occupé ce poste que durant une année (2016-217), et tu peux te faire une idée de son action à partir des comptes rendus qu'il a faits sur leur mailing-list.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je viens de m'apercevoir que j'ai écorché le nom d'un des candidats : le DPL sortant s'appelle Medhi (et non Medi) Dogguy.

Toutes mes confuses.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne sais pas comment on est arrivé au modèle actuel, mais je vois bien pourquoi on n'a pas pu le changer jusqu'à maintenant:

Les 2 plus gros partis, qui gagnent alternativement quasiment toutes les élections, n'ont absolument aucun intérêt à changer un système qui favorise… les 2 plus gros partis!

Il se peut que tu prennes là l'effet pour la cause. Le mode de scrutin uninominal ne peut parfaitement représenter la volonté majoritaire qu'en la présence de deux alternatives, raison pour laquelle il pousse aux alliances et au bipartisme.

Pour ce qui est des raisons qui ont amené ce modèle, il se peut que ce soit de bêtes problèmes d'ordre logistique. De mémoire, Condorcet et Borda, qui avait fort bien analysé les problèmes de ce mode de scrutin, dans leurs mémoires où ils exposaient des méthodes alternatives ont pointés du doigt la plus grande complexité d'organisation du vote selon leur principe. Cela étant, cela n'a nullement empếché d'autres pays de s'en inspirer et de ne pas pratiquer le scrutin uninominal.

Enfin, pour l'anecdote, je n'ai plus grand espoir de voir le mode de scrutin changer en France, mais on ne sait jamais. Lors de l'élection de 2002 j'avais prévenu mon entourage des dangers que représentait le grand nombre de candidats au premier tour et le risque d'éparpillement des voix; j'ai obtenu pour réponse : la politique c'est pas des mathématiques ! Suite au résultat du premier tour, aucune prise de conscience : le mode de scrutin ne pose aucun problème. Dans la foulée, un ami qui effectuait sa thèse en science politique organise une conférence avec politologues et sondeurs (qui défendaient leur chapelle sur leurs « erreurs de prédiction ») pour essayer d'analyser et de comprendre le résultat de l'élection. Au moment des questions du public, rebelote, je remets sur le tapis la question du mode de scrutin et là, réaction identique et unanime : où est le problème avec notre mode de scrutin ? il n'y a aucune raison de le changer !

Je doute, par expérience, que la résistance au changement proviennent des deux gros partis, mais bien plutôt des électeurs eux-mêmes qui ne voient pas que le mode de scrutin pose problème.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tu sembles ignorer un peu les sources d'informations contradictoires. Mais c'est un choix courant à notre époque.

Pour continuer à t'aider dans l'équilibre des sources d'informations, voici une autre vidéo issue de la même chaîne que la tienne : Mélenchon, hommage à Fidel Castro. Et quel grand démocrate ce Fidel !

Mais il est vrai que l'on peut y déceler toute la subtilité de Jean-Luc, ce fin rhéteur, lorsqu'il fustige l'embargo portant sur 20% de l'économie cubaine (vers 3min 30). En effet, comment ne pas lire entre ligne et constater que, sous des faux semblants, il cherche en réalité à faire l'éloge du libre-échange entre les nations. :-D

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai regardé un peu la documentation de Idris et je ne suis pas convaincu que cela simplifie les choses par rapport à Coq.

Une des fonctionnalité centrale des langages avec types dépendants (les types sont des citoyens de première classe, comme les fonctions le sont dans les langages fonctionnels) est de pouvoir prouver des théorèmes de spécification et de correction sur les programmes. Or quand je lis les deux exemples de la documentation : l'addition est associative sur les entiers et l'addition est commutative, je ne trouve pas cela plus simple. Il faut écrire un module dans un fichier avec une preuve laissée indéterminée, chargé le module dans la REPL, utiliser les tactiques pour effectuer la preuve puis recopier le script de preuve dans le fichier.

Avec CoqIde, pour la preuve d'associativité j'écris cela dans un fichier :

(* je remets la définition du type nat et de la fonction plus *)
Inductive nat :=
  | O : nat
  | S : nat -> nat.

Fixpoint plus n m :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.

Infix "+" := plus.

(* pour ce qui est des tactiques utilisées dans la preuve,
   j'utilise les même que dans la documentation de Idris *)
Theorem plus_assoc : 
  forall n m p, n + m + p = n + (m + p).
Proof.
  induction n.
  - simpl. trivial.
  - simpl. intros. rewrite IHn. trivial.
Qed.

Les preuves en Coq ou Idris peuvent se paraphraser ainsi :

On prouve le théorème par récurrence sur l'entier n.

• Si n = 0 alors après simplification il faut prouver que m + p = m + p ce qui est trivial.
• Ensuite si n = S n' alors il faut montrer S n' + m + p = S n' + (m + p), ce qui revient, par définition de la fonction plus, à montrer que S (n' + m + p) = S (n' + (m + p)) (c'est là l'appel à la tactique simpl qui effectue des réductions de calcul à partir de la définition de plus). Or, d'après l'hypothèse de récurrence on a n' + m + p = n' + (m + p), il suffit donc de montrer S (n' + (m + p)) = S (n' + (m + p)) (là c'est la série intros. rewrite IHn) ce qui est trivial.

Avec un peu de pratique, on peut factoriser les parties communes entres les deux cas de la preuve par récurrence est aboutir à cette preuve :

Theorem plus_assoc : 
  forall n m p, n + m + p = n + (m + p).
Proof.
  induction n; simpl; [|intros; rewrite IHn]; trivial.
Qed.

Les preuves se construisent pas à pas comme décrit dans la documentation de Idris et elles ne semblent pas plus compliquées à effectuer. Je dirais même que vu l'éventail de tactiques disponibles de base avec Coq, elle sont même sans doute plus simple. Exemple :

Require Import Omega.
Theorem thm1 :
  forall n m p, n <= m -> p + n <= p + m.
Proof.
  intros; omega.
Qed.

Ensuite, il y a un point qui me chagrine dans l'article de présentation de Edwin Brady. Au paragraphe 3.5 page 14, il écrit :

3.5 Metatheory
We conjecture that TT respects the usual metatheoretic properties, as shown in Figure 5.

Ici c'est moi qui graisse, parce que pour le Calcul des Constructions Inductives (qui est à Coq ce que TT est à Idris) on n'en est pas au stade de la conjecture mais d'un résultat établi. Est-ce bien une conjecture pour TT ou le résultat a été prouvé ?

De plus, même si je peux comprendre le choix fait pour contrôler si les fonctions définies sont totales ou partielles (paragraphe 3.6), il est plus strict que celui de Coq qui permet de définir des fonctions totales qui seront considérées (à tort) comme partielles par Idris (d'un autre côté en Coq il n'y a pas le choix : les fonctions sont toutes totales).

Pour apprendre en douceur et progressivement la programmation en Coq lorsque l'on vient de la programmation fonctionnelle sans type dépendant (Haskell ou OCaml, par exemple), à mon avis le plus simple est de lire le livre (en anglais) Software Foundations de Benjamin C. Pierce disponible en ligne avec le code associé. D'ailleurs le livre est écrit en Coq et la version htlm est générée via l'utilitaire coqdoc.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Certes, mais même lorsque l'on fait du typage statique et que l'on utilise un algorithme d'unification, il est possible de renvoyer des messages plus compréhensibles. Le papier auquel tu renvoies donne des pistes, mais le message de Guillaume Denry sur elm est encore plus parlant. Elm a un système de type à la Haskell et son message d'erreur est on ne peut plus compréhensif et informatif.

Comme ces derniers temps je joue un peu avec Coq, qui doit faire face à des problématiques d'unification à coté desquelles celles de Rust sont un jeu d'enfant, je vais donner des exemples dans ce langage.

Pour commencer, il semblerait naturel de n'utiliser une notation infixe x + y que dans une structure de monoïde. Alors je vais le faire façon type classes à la Haskell :

Class monoid {A : Type} (op : A -> A -> A) (e : A) := {
  _ : forall x y z, op x (op y z) = op (op x y) z ;
  _ : forall x, op e x = x ;
  _ : forall x, op x e = x }.

Generalizable Variables A op e.

Definition monoid_op `{M : monoid A op e} x y := op x y.

Infix "+'" := monoid_op (at level 50).

Là on fait un type checking sur la fonction monoid_op :

Check monoid_op.
(* ==>
monoid_op
     : ?A -> ?A -> ?A
where
?A : [ |- Type] 
?op : [ |- ?A -> ?A -> ?A] 
?e : [ |- ?A] 
?M : [ |- monoid ?op ?e] *)

Elle prend deux valeurs d'un certain type ?A et renvoie une valeur de ce type, et cela dans un contexte où ce type est connu avec un monoïde sur les valeurs de ce type (le ? signifie que le terme est indéterminé, la variable est existentielle : il existe une valeur A telle que …). Si on lui demande de typer l'expression 1 +' "3a", on obtient :

Check 1 +' "3a".
(* ==>
Error:
The term ""3a"" has type "string" while it is expected to have type "nat". *)

Mais le plus amusant est qu'il peut typer le terme "1" +' "3a" avant même de savoir le calculer :

Check "1" +' "3a".
(* ==>
"1" +' "3a"
     : string
where
?op : [ |- string -> string -> string] 
?e : [ |- string] 
?M : [ |- monoid ?op ?e] *)

Eval compute in "1" +' "3a".
(* ==>
     = ?op "1" "3a"
     : string *)

Maintenant pour lui permettre de calculer, on lui fournit une instance de la classe :

(* on prouve que le type string muni de l'opération de concaténation
   est un monoïde dont l'élément neutre est la chaîne vide. *)
Instance Str_append : monoid append "".
Proof.
split.
- induction x; [auto | intros; simpl; rewrite IHx; reflexivity].
- reflexivity.
- induction x; [auto | simpl; rewrite IHx; reflexivity].
Qed.

(* maintenant on vérifie le type et on évalue : *)
Check "1" +' "3a".
(* ==>
"1" +' "3a"
     : string *)

Eval compute in "1" +' "3a".
(* ==>
     = "13a"
     : string *)

Pour le cas plus général où les deux opérandes ne sont pas du même type (et l'on se demande bien alors pourquoi utiliser la notation additive ?), et revenir à la situation de python, je vais l'illustrer ainsi.

Class bin_op (A B C : Type) := op : A -> B -> C.

Infix "+'" := op (at level 50).

Check 1 +' "3a".
(* ==>
1 +' "3a"
     : ?C
where
?C : [ |- Type] 
?bin_op : [ |- bin_op nat string ?C] *)

Là on est dans la situation de python : comme il fait du typage dynamique, lors de l'appel au calcul de l'expression il vérifie si l'environnement permet de bien typer le terme (s'il peut instancier ces variables existentielles). Comme ce langage permet de modifier dynamiquement l'environnement, il est impossible de refuser statiquement ce code. Il pourrait, par exemple, être défini dans une bibliothèque où le code ne peut être évalué, puis importer dans un code qui rend l'évaluation possible. Comme dans le dialogue suivant avec la REPL Coq :

Eval compute in 1 +' "3a".
(* ==>
     = ?bin_op 1 "3a"
     : ?C *)

(* ici l'évaluation totale génère une erreur : le typage étant statique,
   il exige d'être dans un environnement où les variables existentielles
   sont instanciées. *)
Eval vm_compute in 1 +' "3a".
(* ==>
Error: vm_compute does not support existential variables. *)

Instance nat_add : bin_op nat nat nat := {op := plus}.
Instance str_app : bin_op string string string := {op := append }.
Instance nat_str : bin_op nat string string := {
  op n s:=
    match get n s with 
    | None => ""
    | Some c => String c ""
    end }.

Eval vm_compute in 1 +' 3. (* ==> 4 : nat *)
Eval vm_compute in "1" +' "3a". (* ==> "13a" : string *)
Eval vm_compute in 1 +' "3a". (* ==> "a" : string, à la manière du C *)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

L'analyse polyédrique a été proposée pour l'optimisation et la parallélisation en compilation depuis la fin des années 80

Cela confirme une partie de la discussion qui suit la conférence : il semblerait que ce soit le bug d'Ariane V qui ait amené à s'intéresser à ce genre de technique.

Je ne me suis jamais penché sur la complexité de ce type d'algorithme, mais j'ai une question sur deux de tes remarques :

Mais utiliser un solveur ILP mène à de sérieuses contraintes, entre autres que le temps de résolution des (in)équations augmente exponentiellement avec la complexité du nid de boucle à paralléliser/optimiser.

et

Bref. Pour passer d'un modèle mathématique correct, et qui fonctionne sur des programmes/boucles jouet, à un compilateur qui peut compiler du « vrai » code (principalement scientifique), il a fallu attendre environ 20 ans (et sacrifier pas mal de thésards à l'autel du modèle polyédrique).

Les cas pathologiques pour la complexité exponentielle, on les rencontres dans du « vrai » code ? Je pose la question parce que, pour revenir sur le thème du journal et les ADT, ce système de type et son mécanisme d'inférence est basé sur l'algorithme d'unification de Robinson (milieu des années 1960) et le système Hindley-Milner ou le système F (début des années 70). Pour l'étude de la compléxité, il a fallu attendre 1991 et elle est doublement exponentielle. Xavier Leroy en propose une étude dans son livre sur le langage Caml (page 360 du livre et 370 du pdf). Cela étant, dans la « vraie » vie, sur du « vrai » code, on observe que l'algorithme se comporte linéairement : quand on double la taille du programme, on double le temps de compilation. Les pires cas en compléxité temporelle sont pathologiques; et à mon avis un programmeur qui les écriraient auraient soit l'esprit totalement tordu, soit aurait le cerveau qui exploserait bien avant de faire chauffer son CPU pour essayer de comprendre son propre code.

P.S : pour la vidéo, je les regarde en streaming via le lecteur proposé sur la page en question. Mais plus que la présentation des différentes techniques d'analyse statique, ce que je trouve intéressant c'est la discussion avec le public qui suit la présentation.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Oui, c'est bien la méthode B et l'atelier B qui est derrière tout ça. C'est un successeur du formalisme Z qui a inspiré le langage Eiffel et sa programmation par contrat.

Son inventeur, Jean-Raymond Abrial, est revenu sur l'histoire de ces approches dans une conférence au Collège de France dont voici la présentation :

Cette présentation est celle d’un chercheur vieillissant qui porte un regard historique sur les trente dernières années de son travail.

Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques. Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le même genre d’investigations, à savoir la spécification et la construction vérifiée de systèmes informatisés.

Ce travail, autant théorique que pratique, s’est concrétisé au cours de toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas, loin de là, le seul contributeur). Je vais tenter d’expliciter comment les idées que contiennent ces formalismes et les outils correspondants ont lentement émergés de façon parfois erratique.

Je tenterai aussi de préciser les multiples influences qui ont participé à cette évolution. En particulier, je montrerai comment plusieurs réalisations industrielles ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et parfois les rejets de la part de communautés tant universitaires qu’industrielles.

Pour finir, je proposerai quelques réflexions et approches pour le financement de recherches telles que celle-ci.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Sur un simple enregistrement variant, l'information n'est pas portée avec le type dans la signature d'une fonction. Je peux comprendre qu'on puisse préférer que le compilateur refuse tout simplement de compiler lorsque la vérification est hors de portée.

Si la vérification est hors de portée du compilateur (avec une pleine certitude), alors il ne doit pas refuser de compiler (tout au plus, peut-il émettre un avertissement pour signaler ce qu'il ne peut savoir au cas où cela pourrait poser un problème au développeur) mais prendre des précautions en plaçant un test à l'exécution (ce qui semble être le cas).

J'ai réfléchi, depuis, à cet exemple en ADA et l'impossibilité pour le compilateur de suivre le bon typage d'une telle valeur vient peut être de sa mutabilité. Dans ton exemple, on voit bien qu'il y a là un problème. Mais, de ce que j'ai compris, cette variable pourrait se voir attribuer une valeur connue dynamiquement (après calcul d'une fonction par exemple) qui serait du bon type et possédant, cette fois, le champ en question.

Avec les ADT (même avec des valeurs mutables, comme en OCaml) ce n'est pas possible, car l'existence du champ est marquée par le constructeur de type qu'il faut nécessairement déconstruire.

type politique =
  | NbreFixe of int
  | NbreMaxHardware
  | PasDeThreading
  | CasParticulier;;

(* ici le terme est une variable mutable *)
let ma_politique = ref CasParticulier;;
let _ = ma_politique := NbreFixe 3;;

let i = match !ma_politique with
  | NbreFixe n -> n
  | _ -> assert false
val i : int = 3

Oups, désolé, je ne sais plus comment on a réussi à dériver d'une discussion qui par du compilateur Haskell pour finir par parler des langages objets. Toute mes excuses pour des propos qui auraient pu être interprétés comme blasphématoires dans ce fil de discussion de conviction plutôt fonctionnelle.

Il n'y a rien de blasphématoires dans ce fil, c'est toujours intéressant de voir comment une problématique peut être abordée dans d'autres langages et paradigmes. Et comme je l'avais signalé dans la dépêche sur le compilateur 4.03 de OCaml, c'est du code ADA qui fait tourner les lignes automatiques du métro parisien ;-) (même s'il n'a pas été écrit à la main, mais généré à partir d'un langage plus haut niveau).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Désolé si mon message a pu paraître agressif, telle n'était pas mon intention. C'est juste que je ne voyais pas où tu voulais en venir, ni le rapport avec les discussions du journal et des commentaires qu'il a suscités. Ma réaction était du même ordre que la fameuse réplique :

-- il dit qu'il a plus de genoux
-- il dit qu'il voit pas le rapport.

L'exemple central du journal tourne autour des garanties statiques que peut apporter Haskell (ou plus généralement, le système des ADT) pour la conception d'API et éviter les erreurs à l'exécution. S'en est suivi différentes discussions, avec des illustrations en ADA, Haskell ou OCaml, qui tournent toutes autour de ce même thème : peut-on (et si oui comment ?) contrôler la bonne formation des termes à la compilation (statiquement), ou doit-on mettre des gardes-fous et des tests lors de l'exécution (dynamiquement) ?

Ainsi lorsque je parlais d'outils d'analyses statiques, je ne considérais que ceux dont l'objectif se situe dans la gestion de cette problématique. C'est pour cela qu'à chacune de mes réponses, j'ai rappelé le contexte de la discussion. Je ne sous-entendais pas que les outils d'analyses de code se limitaient à gérer cette question. Et pour tous les cas d'usages que tu mentionnes, cela n'aurait d'ailleurs aucun sens d'avoir une alternative pour les traiter dynamiquement.

Une petite précision pour conclure :

Comme tu dis régulièrement que tu n'es pas développeur et que tu ne connais pas « l'industrie » ça ne me surprenait pas que tu ne connaisse pas ce pan là.

Il est vrai que je ne suis pas développeur (bien que je saches programmer, mais c'est loin d'être ma préoccupation première), et que je ne connais pas l'industrie. Mais quand je dis cela, c'est surtout pour exprimer que je ne sais pas ce qui est passé des laboratoires de recherche (et qui y est notoirement connu) vers le domaine industriel, ni le vocabulaire associé et le changement de dénomination qu'ont pu subir les notions lors du passage (ce qui est aussi parfois le cas lorsque la notion passe du domaine des mathématiques pures et de la logique à celui de l'informatique théorique).

Si je prends un exemple pour illustrer la chose. Dans la vidéo de la conférence sur JML (dont le lien était erroné, le voici), l'orateur expose sur un cas particulier une méthode d'analyse statique dite analyse polyédrique (vers la 40ème minute). Il conclue l'étude de cette exemple avec une diapo qui contient ce passage :

Principe de l'analyse de programme :

• traduction vers un flux d'équation sur des ordres partiels
• résolveur général basé sur des itérations

et la méthode de résolution (comme il le souligne à l'oral) est en partie fondée sur des travaux de Tarski qui datent des années 1930. Résultats auxquels j'avais fait allusion dans un autre journal. Ce type de technique se retrouve dans les solveurs SMT (Satisfiability modulo theories), comme par exemple l'outil alt-ergo (écrit en OCaml) utilisé, entre autre, par Spark dont a parlé Blackknight.

Les résultats de Tarski me sont connus depuis une bonne quinzaine d'années (époque où j'étais étudiant), et ce genre de conférence me permet de savoir que des industriels peuvent en faire usage (quant bien même ils ignoreraient ce qui se trouve sous le capot, ou dans quel contexte et pour quelles raisons ces problèmes ont été résolus à une époque où l'ordinateur n'existait pas encore).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Dans le cas de l'attribut qui n'existe pas selon le discriminant, il n'y aura même pas de Waring à la compilation. Uniquement une Erreur au Runtime. Ça me semble difficile de détecter tous les mauvais usages d'un type variant, surtout si on peut récupérer le record depuis un contexte extérieur (non-Ada). Il faut bien que ça plante quelque part, au niveau de l'interface, si on fait de la programmation par contrat, ou plus loin dans le code si on ne teste pas à l'entrée.

Dans le cas où le code produit peut être utilisé via un autre langage qui ne permettrait pas de détecter statiquement l'erreur, assurément il faut bien alors mettre en place un contrôle dynamique avec émission d'une erreur. Cela relève du principe élémentaire dans le domaine réseau : « be conservative in what you send, be liberal in what you receive ». Ne sachant pas, a priori, ce que le code peut recevoir en entrée, il faut s'attendre à tout et être capable de gérer une erreur à l'exécution. Mais dans ton cas, le code est utilisé dans un contexte ADA et l'erreur est repérable statiquement. Détecter, dans ce cas, tous les mauvais usage d'un type variant à la compilation n'est pas une chose difficile : c'est le principe même du type checking, tâche qui incombe au compilateur dans les langages à typage statique.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Et justement, je dis que les analyseurs statiques servent aussi à refuser du code qui fonctionne parfaitement, mais qui ne correspond pas aux normes défini dans le programme en question par exemple.

Soit mais là on est un plus dans un problème de définition de terme : je ne dispute jamais des mots pourvu que l'on me dise le sens qu'on leur donne.

Mon commentaire était en réponse à un échange entre Guillaum et gerfaut83 au sujet d'un bout de code ADA et du comportement du compilateur. Guillaum s'étonnait de l'absence de garantie statique (absence d'erreur de typage à la compilation), ce à quoi gerfaut83 lui a répondu qu'on se trouvait à la limite entre le travail du compilateur et celui d'un analyseur statique.

Je réponds alors : le type checking (tache qui incombe au compilateur) c'est de l'analyse statique; et dans l'exemple donné il y a clairement un problème de typage qui peut être détecté statiquement, c'est-à-dire à la compilation. Puis j'illustre mon propos sur un exemple pour montrer en quoi cela peut être utile : réduire l'overhead à l'exécution. Comme la chose est vérifiée une bonne fois pour toute à la compilation, il n'est pas nécessaire de faire un test dynamiquement qui générera une exception.

Ensuite, répondre que l'on peut faire rentrer dans la catégorie des tâches dévolues à l'analyse statique d'autres problématiques que le contrôle d'erreurs est hors de propos. Généraliser le concept de l'analyse statique au-delà du cas d'étude ici discuté fait de ton objection une sorte de stratagème III : la généralisation des arguments adeverses :

Il s’agit de prendre une proposition κατα τι, relative, et de la poser comme απλως, absolue ou du moins la prendre dans un contexte complètement différent et puis la réfuter. L’exemple d’Aristote est le suivant : le Maure est noir, mais ses dents sont blanches, il est donc noir et blanc en même temps. Il s’agit d’un exemple inventé dont le sophisme ne trompera personne. Il faut donc prendre un exemple réel.

Exemple 1

Lors d’une discussion concernant la philosophie, j’ai admis que mon système soutenait les Quiétistes et les louait. Peu après, la conversation dévia sur Hegel et j’ai maintenu que ses écrits étaient pour la plupart ridicules, ou du moins, qu’il y avait de nombreux passages où l’auteur écrivait des mots en laissant au lecteur le soin de deviner leur signification. Mon adversaire ne tenta pas de réfuter cette affirmation ad rem, mais se contenta de l’argumentum ad hominem en me disant que je faisais la louange des Quiétistes alors que ceux-ci avaient également écrit de nombreuses bêtises.

J’ai admis ce fait, mais pour le reprendre, j’ai dit que ce n’était pas en tant que philosophes et écrivains que je louais les Quiétistes, c’est-à-dire de leurs réalisations dans le domaine de la théorie, mais en tant qu’hommes et pour leur conduite dans le domaine pratique, alors que dans le cas d’Hegel, nous parlions des ses théories. Ainsi ai-je paré l’attaque.

Les trois premiers stratagèmes sont apparentés : ils ont en commun le fait que l’on attaque quelque chose de différent que ce qui a été affirmé. Ce serait un ignoratio elenchi de se faire battre de telle façon. Dans tous les exemples que j’ai donnés, ce que dit l’adversaire est vrai et il se tient c’est en opposition apparente et non réelle avec la thèse. Tout ce que nous avons à faire pour parer ce genre d’attaque est de nier la validité du syllogisme, c’est-à-dire la conclusion qu’il tire, parce qu’il est en tort et nous sommes dans le vrai. Il s’agit donc d’une réfutation directe de la réfutation per negationem consequentiæ.

Il ne faut pas admettre les véritables prémisses car on peut alors deviner les conclusions. Il existe cependant deux façons de s’opposer à cette stratégie que nous verrons dans les sections 4 et 5.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Toutes les discussions que l'on voit au dessus montrent justement qu'il y a suffisamment de façon de résoudre un problème pour que ça ne soit pas figé dans le langage. Pour autant tu peux vouloir, au sein d'un programme donné, n'autoriser qu'une seule solution à fin d'améliorer la cohérence.

Où vois-tu dans mon propos que c'est figé dans le langage ? La discussion portait sur un bout de code ADA, celui-ci :

MaPolitique := (Politique => CasParticulier);
MaPolitique.NombreThread := 5; -- CONSTRAINT_ERROR : discriminant check failed

qui générera une exception à l'éxecution car, dans ce cas du variant, il n'y a pas de champ NombreThread. C'est là une problématique de typage, et d'ailleurs le compilateur semble savoir qu'il y a problème, mais la norme semble avoir préférée émettre un warning et non une erreur de compilation. D'où la question de Guillaum : « Il n'y a pas de garantie statique sur ce genre de chose ? Ça c'est dommage ». Question à laquelle gerfaut83 a répondu : « J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code ».

D'une manière générale, le principe du typage statique se situe dans la question : comment refuser d'exécuter un code qui plantera nécessairement ? ou plutôt, comment savoir qu'un bout de code plantera nécessairement avant de le lancer ? D'où mon exemple pour refuser statiquement, par contrainte de type, un arbre vide comme entrée pour une fonction plutôt que de générer une exception à l'exécution; solution qui de plus réduit l'overhead du code généré.

Dans l'exemple ci-dessus, ce n'est pas tant une impossibilité d'inférer statiquement qu'il y aura un problème, mais un choix de la norme qui considère cela comme un avertissement et non comme une erreur critique. Mais dans bien des cas, sans ajout d'informations qui ne sont pas définies par le langage, il n'est pas possible de garantir certains invariants d'un code. Ce à quoi je faisais référence, pour aborder cette problématique, était des outils d'analyse statique comme JML pour Java présenté, par exemple, dans la conférence Intégration de la vérification formelle dans les langages de programmation.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code.

Certes, mais le contrôle de type (type checking) effectué par un compilateur relève de l'analyse statique de code. Dans les faits, on ajoute des outils d'analyse statique de code à l'extérieur du compilateur pour pallier aux déficiences du système de types d'un langage. Et pour fonctionner, ces outils nécessitent habituellement l'ajout d'annotations au code sous forme de commentaires, annotations qui correspondent à un enrichissement du langage des types du langage de départ.

Dans tout langage de programmation, il y a en réalité deux langages :

• le langage des termes pour décrire les calculs à effectuer ;
• le langage des types pour rejeter à la compilation, ou à l'exécution, certains termes comme sémantiquement invalides (vides de sens).

Plus le langage des types est évolué, plus il permet de contrôler la bonne formation des termes à la compilation (c'est-à-dire statiquement). L'idée des ADT est de pouvoir effectuer du raisonnement par cas non sur la valeur des termes (ce qui ne peut se faire qu'à l'exécution, là où la valeur est connue) mais sur leur type (ce qui est connu statiquement à la compilation).

On peut même pousser le principe plus loin avec des GADT pour discriminer plus fortement la construction des termes, et faciliter l'optimisation du code généré sans avoir à gérer d'exception au runtime. Je vais l'illustrer sur un exemple en OCaml avec une fonction qui retourne la valeur du nœud racine d'un arbre binaire parfait.

Avec les ADT, on peut encoder les arbres binaires parfaits ainsi :

type 'a t =
  | Empty : 'a t
  | Node : 'a * ('a * 'a) t -> 'a t

Les contraintes sur le type ne permettent que de construire des arbres parfaits : soit l'arbre est vide, soit c'est un nœud qui contient une valeur de type a et un arbre paramétré par un couple de type 'a * 'a (ce qui représente les sous-arbres gauche et droite).

Pour extraire, la valeur du nœud racine on procède ainsi :

let top = function
  | Empty -> failwith "Empty tree"
  | Tree (v, _) -> v

La fonction retournera une exception à l'exécution si on lui passe un arbre vide :

top Empty;;
Exception: Failure "Empty tree".

Maintenant, avec les GADT, on peut encoder ce type d'arbre ainsi :

type z = Z
type 'n s = S : 'n -> 'n s

type ('a, 'n) t =
  | Empty : ('a, z) t
  | Tree : ('a, 'n) t * 'a * ('a, 'n) t -> ('a, 'n s) t

Ici, c'est plus subtil et plus précis au niveau des contraintes de types. On commence par encoder les entiers dans le système de type avec z pour représenter zéro, et 'n s pour représenter la fonction successeur. Ensuite, on paramètre le type des arbres à la fois par le type des nœuds ('a) ainsi que par sa profondeur ('n). La définition dit qu'un arbre vide est de profondeur nulle et que les sous-arbres d'un nœud ont la même profondeur 'n (l'arbre est parfait) et que sa profondeur est 'n + 1 = 'n s.

Pour coder la fonction top, il est n'est plus nécessaire de traiter le cas de l'arbre vide :

let top : type a n. (a, n s) t -> a = function
  | Tree (_, v, _) -> v

Le type de la fonction déclare explicitement que la profondeur de l'arbre est du type successeur ('n s) et donc l'arbre ne peut être vide. Cette fois, si on lui passe un arbre vide, on a une erreur de typage à la compilation :

top Empty;;
Error: This expression has type ('a, z) t
       but an expression was expected of type ('a, 'b s) t
       Type z is not compatible with type 'b s

Pour ce qui est du code généré par le compilateur (option -dlambda du compilateur), on peut vérifier qu'il peut faire l'économie d'un test à l'exécution.

Avec ADT, on obtient :

let 
  (top =
    (function p
      (if p (field 0 p)
        (apply (field 1 (global Pervasives!)) "Empty tree"))))

Avec les GADT, on a :

let (top = (function p (field 1 p))

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Réserve partagée sur l'abus d'opérateurs ; cela dit, les parenthèses à la Lisp ne demandent pas de moindres efforts non plus.

C'est sans doute une question d'habitude. Je ne connais pas les règles de précédences des opérateurs infixes en Haskell mais, à partir des types des fonctions et des constructeurs, j'ai eu plus de facilité à lire ta version à celle avec parenthèses. J'ai du relire une deuxième (voire troisième) fois la version à la lisp pour bien me repérer; là où j'ai compris ton code à la première lecture.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Au temps pour moi, j'avais mal compris ce que tu voulais dire par là. Fréquentant peu le milieu des développeurs (que je lis surtout ici), je ne savais pas que les solutions orientées fonctionnelles étaient à la mode. De toute façon, les modes ça passe et ça repasse. ;-)

Cela étant, j'ai du mal à considérer les jugements disjonctifs et conjonctifs comme des notions sophistiquées. Ce qu'il y a, c'est qu'en POO la disjonction est abordée par la subdvision des concepts : l'héritage est un processus de spécification d'un genre (comme dans la proposition « un animal est un chien ou un chat ou une girafe… ») qui, comme l'a rappelé Guillaum, est ouvert par essence (nul ne peut dire a priori, c'est-à-dire statiquement, jusqu'où peut s'arrêter la spécification). L'avantage de la subdvision par les ADT est de fournir une partition exhaustive du type à diviser, et donc de pouvoir vérifier statiquement que tous les cas sont traités lors de la manipulation d'une valeur d'un tel type.

Comme l'a également rappelé Guillaum, les unions du C sont proches des ADT. Ce qu'il y a peut être de nouveau pour certains développeurs, c'est le vocabulaire employé pour qualifier ce genre de types : types de données algébriques. C'est lié aux relations que la disjonction et la conjonction entretiennent entre elles, et la façon dont elles opèrent l'une sur l'autre. Dans un choix comme celui d'un menu : (entrée et plat ) ou (plat et dessert), c'est équivalent au choix : plat et (entrée ou dessert). Ce qui n'est rien d'autre que la règle de distributivité de la multiplication sur l'addition : plat * (entrée + dessert) = (plat * entrée) + (plat * dessert).

En revanche, sur ce point :

Oui alors les types dépendants c'est une logique qu'un gamin de 4 ans comprends tout à fait.

je crois que tu surestimes grandement les capacités des enfants de 4 ans. ;-)

D'après mon expérience, un enfant de cet âge comprend tout à fait la logique propositionnelle (conjonction, disjonction et implication), c'est à dire celle qui sert de fondement au système de type de Haskell ou OCaml, mais ne sait pas raisonner si on introduit les notions de sujets et prédicats. Usuellement, on a plutôt fixé l'âge de raison à 7 ans; et encore même à 7 ans ce n'en est que des balbutiements.

Dans l'actualité récente, l'idée d'introduire les notions de sujet et prédicat dans les leçons de grammaire à partir des classes de CM1 a fait couler beaucoup d'encre : L'introduction du prédicat va-t-elle vraiment appauvrir la grammaire française ?. L'article est intéressant à lire, même si la notion n'est pas encore très claire pour son auteur. Comme dans l'exemple qu'il donne au début :

Par exemple, dans «cette polémique est totalement absurde», «cette polémique» est le sujet ; «est totalement absurde» est le prédicat, c’est-à-dire la partie de la phrase qui dit ce que le sujet fait ou est.

Ici le sujet est bien « cette polémique », mais le prédicat est « totalement absurde ». L'auxiliaire « être » constitue ce que l'on appelle la copule du jugement, c'est-à-dire la forme, là où le sujet et le prédicat en sont la matière. Comme dans le jugement suivant :

let l = [1; 2; 3];;
val l : int list = [1; 2; 3]

Le sujet est l, le prédicat int list et la copule est signifiée par le : entre eux. Ce que l'on exprimerait en français par la proposition : « la valeur l est une liste d'entiers ».

En revanche, les types dépendants ou leur forme affaiblie que sont les GADT ressemblent plus à des systèmes de types que je qualifierais de sophistiqués. Comme dans l'exemple suivant avec des GADT pour encoder la taille d'une liste dans son type.

module Llist = struct
  type z = Z (* zéro *)
  type 'n s = S : 'n -> 'n s (* la fonction successeur *)

  type un = z s (* un est le successeur de zéro *)
  type deux = un s (* deux est le successeur de un *)
  type trois = deux s (* trois est le successeur de deux *)

  type ('a,'n) t =
    | [] : ('a, z) t
    | (::) : 'a * ('a, 'n) t -> ('a, 'n s) t

  let rec zipwith :
    type a b c n. (a -> b -> c) -> (a, n s) t -> (b, n s) t -> (c, n s) t =
    fun f l l' -> match l, l' with
      | x :: [], x' :: [] -> (f x x') :: []
      | x :: y :: l, x' :: y' :: l' ->
          (f x x') :: zipwith f (y :: l) (y' :: l')
end;;
module Llist : sig
    type z = Z                                                                  
    type 'n s = S : 'n -> 'n s                                                  
    type ('a, 'n) t = [] : ('a, z) t | (::) : 'a * ('a, 'n) t -> ('a, 'n s) t   
    val zipwith :                                                               
      ('a -> 'b -> 'c) -> ('a, 'n s) t -> ('b, 'n s) t -> ('c, 'n s) t          
end

Ici on a des listes chaînées encodées via un GADT avec deux paramètres de types : a qui exprime le type homogène des éléments de la liste et n qui exprime la longueur de la liste (on encode les entiers dans le système de types via une représentation unaire, ce qui convient bien aux listes). Ainsi la fonction zipwith prend une fonction à deux paramètres et deux listes de valeurs, puis renvoie la liste des valeurs prises par la fonction. Mais ici, grâce au GADT, on peut exprimer dans le type de zipwith que les deux listes doivent être non vide et de même longueur (paramètre de type n s), sous peine de déclencher une erreur de typage à la compilation et non une erreur à l'exécution.

open Llist;;

let l : (int, deux) t = 1 :: 2 :: []
and l1 : (int, deux) t = 2 :: 3 :: []
and l2 : (int, trois) t =1 :: 2 :: 3 :: [];;

zipwith (+) l l1;;
- : (int, un s) t = :: (3, :: (5, []))

(* erreur à la compilation avec l de longueur 2 et l2 de longueur 3 *)
zipwith (+) l l2;;
Error: This expression has type (int, trois) t
       but an expression was expected of type (int, un s) t
       Type trois = deux s is not compatible with type un s 
       Type deux = un s is not compatible with type un = z s
       Type un = z s is not compatible with type z

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

La question naïve c’est en quoi les ADT sont mieux que l’héritage et les méthodes virtuelles ?

La question pour moi, au départ, est : que cherche-t-on à exprimer ? Quelles sont les relations que l'on pense (avant d'écrire et exprimer sa pensée, il faut d'abord la constituer et la structurer) entre les structures de données ? Ici, il s'agit de rapport disjonctif et conjonctif : union disjointe et produit cartésien d'ensembles (comme dans le cas d'un menu au restaurant : entrée-plat ou plat-dessert).

Ces précisions faites, à ta question je répondrai : ADT ou héritage et méthodes virtuelles, relativement à la problématique exposée, c'est bonnet blanc et blanc bonnet. Le couple héritage et méthodes virtuelles est le moyen pour exprimer des ADT dans les langages orientés objets. La seule différence avec les langages fonctionnels, c'est que c'est plus verbeux. D'où ma conclusion : c'est quelque peu aberrant de devoir faire des circonvolutions pour exprimer une telle pensée.

type entree = (* ... *)
type plat = (* ... *)
type dessert = (* ... *)

type menu =
 | A : entree * plat -> menu
 | B : plat * dessert -> menu

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je sais que c'est moins hype que de décrire des typages sophistiqués, mais des factories font ça très bien.

Je ne vois pas en quoi l'approche par ADT est hype ou sophistiquée. Le principe même, à la base des ADT, consiste dans certaines formes logiques des jugements : la disjonction (exclusive) et la conjonction. Un jugement disjonctif, c'est hype et sophistiqué ? Quand un serveur, au restaurant, te demande si dans le menu tu as choisi l'option entrée et plat (conjonction, ou type produit) ou (disjonction ou type somme) plat et dessert, tu trouves cela hype et sophistiqué ?

Personnellement, ce que je trouve aberrant, c'est de devoir faire des circonvolutions pour exprimer des jugements de typage aussi triviaux et naturels à l'esprit humain.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Pour rendre deux instances du type 'a P.t incompatibles, en choisissant des types incompatibles pour la valeur du type fantôme (int et float dans les exemples de octachron).

Dans l'usage des modules que j'ai proposé, on avait deux modules A et B dont les types étaient incompatibles : bien que structurellement identiques, comme ils étaient abstraits, les types A.t et B.t étaient incompatibles.

Dans l'approche avec type fantôme, il n'y a qu'un seul module et les types a P.t et b P.t sont rendus incompatibles par un choix adapté du type fantôme. Un des avantages que je vois, au premier abord, par rapport à ma solution, et que cela évite de dupliquer (dans deux modules distincts) les fonctions qui opèrent sur les types en questions. Tu pourrais, par exemple, définir deux type vides :

type abs (*coordonnées absolues *)
type rel  (* coordonnées relatives *)

puis faire un module de coordonnées :

module Coord : sig
  type 'a t
  (* signatures des opérations *)
end = struct
  type 'a t = int * int
  (* défintions des opérations *)
end

et définir tes variables avec des annotations comme cela :

let p_abs : abs Coord.t = (* ... *)
let p_rel : rel Coord.t = (* ... *)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

j'ai une M-Audio Fast Track Pro sous les yeux, qui déjà pour faire certains trucs (genre 24bit / 96kHz) sous Linux a besoin d'un driver spécial (donc PAS plug & play)

Eh, ça m'intéresse !!! :-) T'as un lien vers un tuto pour la faire fonctionner avec cet échantillonage ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Cela dépend beaucoup ce que tu entends par "ce cas" et pouvoir se faire

Je pensais effectivement à l'encodage sous la forme des entiers de Peano. Comme c'est une représentation unaire des entiers, leur taille croît bien linéairement. C'est aussi cet encodage qui est illustré dans le cours de Jeremy Yallop.

L'idée est bien de montrer qu'avec les GADT, on peut avoir une forme affaiblie de type dépendant. Pour avoir des types dépendants complets, il faut passer à des langages comme Coq; mais là, c'est pour les fous ! :-P

Merci pour les deux liens, je regarderai cela à tête reposée.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je pense qu'il est souvent prématuré de se poser des questions de représentation mémoire quand on écrit un programme—à moins de savoir d'avance que le type sera impliqué dans les parties les plus coûteuses en performance.

C'est vrai, d'autant que j'ai parlé trop vite sur le coup mémoire. Là, s'il veut réduire les coûts, il peut garder son code actuel, enlever les parenthèses autour du couple dans sa définition de type et utiliser des fonctions de constructions là où il construisait en partant d'une paire existante.

depuis OCaml 4.04 (Novembre 2016), on peut écrire

type t = Foo of bar [@@unboxed]

pour supprimer l'indirection dans ce cas. (C'est utile pour packer des existentiels sans indirection.)

Je ne connaissais pas cette nouveauté, c'est intéressant.

Par contre, j'ai une question. Lorsque dans le journal, il s'interroge sur :

On peut (doit ?) pousser le concept plus loin, comme par exemple écrire une bibliothèque de calcul matriciel qui vérifie à la compilation la dimensionnalité des calculs.

Ce contrôle statique ressemble à des types dépendants (un type paramétré par une valeur du langage, ici un int pour la dimension des matrices). Pour ce cas, ça doit pouvoir se faire avec des GADT comme dans les exemples du cours de Jeremy Yallop; mais c'est un usage assez avancé du système de type. Me trompe-je ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il est vrai que la notation pour l'application des constructeurs de types inductifs peut apparaître contre intuitive, car elle n'est pas consistante avec celle des fonctions : c'est parce que en OCaml, on ne peut pas faire d'application partielle sur un constructeur de type (contrairement à Haskell, il me semble). Résultat les paramètres se passent entre parenthèses, comme en python par exemple.

Pour la taille mémoire, 5 ou 3 mots, cela se voit ainsi : un type somme occupe 1 mot mémoire qui contient des informations sur entre autre la structure des paramètres, plus 1 mot par paramètre. Ainsi dans le cas Coord of (int * int), on a 1 mot + 1 mot pour le paramètre qui pointe sur une paire int * int, paramètre qui contient lui même 1 mot de « tag » et 1 mot pour chaque int; d'où un total de 5 mots avec une indirection. Dans le cas Coord of int * int, on a 1 mot de « tag » plus 1 mot par paramètre, soit un total de 3 mots.

Si tu veux pouvoir créer une variable de type Coord of int * int à partir d'une paire préexistante, il faut passer par un «smart » constructeur, c'est-à-dire une fonction de qui prend une paire et renvoie une valeur du bon type (à l'instar de mes fonctions make dans mes exemples avec modules).

type coord = Coord of int * int;;
type coord = Coord of int * int

let coord (x,y) = Coord (x,y);;
val coord : int * int -> coord = <fun>

Sinon pour revenir sur l'approche modulaire, un de ses intérêts pourrait être, dans un premier temps, de te familiariser avec le système de module. Ensuite, tu pourrais jeter un œil sur les fonctions qui prennent des modules comme arguments pour retourner des modules, ce que l'on appelle des foncteurs. Comme ton projet consiste à afficher des schémas kicad, je vais comparer cela à l'électronique. Quand tu fais un schéma de circuit, certains composants peuvent être remplacés par d'autres tant qu'ils fonctionnement de la même façon : c'est cela un module, un composant. Et ton foncteur, c'est le schéma de ton circuit qui décrit comment les assembler pour fabriquer un nouveau composant. Si dedans tu as un micro contrôleur, tu peux opter lors de la réalisation entre des modèles de différents fabricants (qui peuvent différer sur leur structure interne) tant qu'ils réalisent la même fonction et exposent la même interface.

Si je reprends mon interface de coordonnées en lui ajoutant quelques fonctions :

module type Coord = sig
  type t
  val make : int -> int -> t                                                  
  val to_pair : t -> int * int
  val move : ?dx:int -> ?dy:int -> t -> t
  val compare : t -> t -> int
end

On peut l'implémenter avec des couples ou des paires (enregistrements) :

module PCoord : Coord = struct
  type t = int * int
  let make i j = (i, j)
  let to_pair p = p
  let move ?(dx = 0) ?(dy = 0) (x,y) = (x + dx, y + dy)
  let compare (i, j) (i', j') =
    let c = compare i i' in
    if c = 0 then compare j j' else c
end

module RCoord : Coord = struct
  type t = {x:int; y:int}
  let make i j = {x = i; y = j}
  let to_pair {x; y} = (x,y)
  let move ?(dx = 0) ?(dy = 0) p = {x = p.x + dx ; y = p.y + dy}
  let compare p p' =
    let c = compare p.x p'.x in
    if c = 0 then compare p.y p'.y else c
end;;

Comme ils définissent un type t et une fonction de comparaison compare, tu peux obtenir directement un module pour gérer des ensembles de coordonnées, en utilisant le foncteur du module Set de la bibliothèque standard :

module F = Set.Make(PCoord);;
module F :
  sig
    type elt = PCoord.t                                                         
    type t = Set.Make(PCoord).t
    val empty : t
    val is_empty : t -> bool
    val mem : elt -> t -> bool
    val add : elt -> t -> t
    val singleton : elt -> t
    val remove : elt -> t -> t
    val union : t -> t -> t
    val inter : t -> t -> t
    val diff : t -> t -> t
    val compare : t -> t -> int
    val equal : t -> t -> bool
    val subset : t -> t -> bool
    val iter : (elt -> unit) -> t -> unit
    val map : (elt -> elt) -> t -> t
    val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
    val for_all : (elt -> bool) -> t -> bool
    val exists : (elt -> bool) -> t -> bool
    val filter : (elt -> bool) -> t -> t
    val partition : (elt -> bool) -> t -> t * t
    val cardinal : t -> int
    val elements : t -> elt list
    val min_elt : t -> elt
    val max_elt : t -> elt
    val choose : t -> elt
    val split : elt -> t -> t * bool * t
    val find : elt -> t -> elt
    val of_list : elt list -> t
  end

Tu peux voir ça comme si ton module offrait plusieurs pins en interface et que tu routes certains d'entre eux (le type t et la fonction compare) vers une partie de ton circuit pour avoir des ensembles. Mais dans la pratique, tu peux choisir un modèle de composant plutôt qu'un autre pour des raisons de performance (bien que dans mon exemple bateau, les deux doivent être sensiblement identiques une fois compilés).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Pas forcément, ça dépend de la manière dont le type est écrit. […]

Intéressant, je ne savais pas qu'il y avait une différence entre les deux écritures au niveau de la représentation mémoire. Je croyais qu'au niveau du compilateur, il y avait juste des passes d'optimisation au niveau des phases de constuction-deconstruction pour réduire le nombre de suivi de pointeurs. Et cette « curryfication » des constructeurs, elle est faite pour tous les types de tuples ?

Edit : c'est bon, j'ai ma réponse dans ton commentaire en réponse à Aluminium.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il existe un autre moyen, pour éviter les alias entre types structurellement identiques, qui consiste à passer par le système de modules et les type abstraits. Ta solution, bien que résolvant ta problématique, rajoute une indirection en mémoire : tes types sont des pointeurs sur des couples de int (qui n'ont pas la même étiquette et ne sont donc pas identiques). Afin d'éviter ce pointeur, on peut utiliser des modules dans lesquels les types seront directement des couples mais en le cachant au monde extérieur.

Exemple :

(* on définit une signature pour un module de coordonnés *)
module type Coord = sig
  type t
  val make : int -> int -> t
  val to_pair : t -> int * int
end

(* on définit deux implémentations identiques *)
module A : Coord = struct
  type t = int * int
  let make i j = (i,j)
  let to_pair x = x
end;;
module A : Coord

module B : Coord = struct
  type t = int * int
  let make i j = (i,j)
  let to_pair x = x
end;;
module B : Coord

Ici, comme l'interface des modules définit un type t sans rien dire sur lui (on parle de type abstrait), les types A.t et B.t sont incompatibles, bien que structurellement identiques.

let p = A.make 1 2;;
val p : A.t = <abstr>

A.to_pair p;;
- : int * int = (1, 2)

(* les types ne sont pas compatibles *)
B.to_pair p;;
Error: This expression has type A.t but an expression was expected of type B.t

Ensuite, il est aisé, à partir des primitives des modules, d'écrire des fonctions de conversions d'un type dans l'autre :

let a_to_b x = let i,j = A.to_pair x in B.make i j;;
val a_to_b : A.t -> B.t = <fun>

let b_to_a x = let i,j = B.to_pair x in A.make i j;;
val b_to_a : B.t -> A.t = <fun>

let p1 = a_to_b p;;
val p1 : B.t = <abstr>

B.to_pair p1;;
- : int * int = (1, 2)

A.to_pair (b_to_a p1);;
- : int * int = (1, 2)

P.S : tout système de types, quelque soit le langage, a à voir avec la preuve de programme, mais là c'est une autre histoire. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.