kantien a écrit 1131 commentaires

une lib Python perso fortement basée sur generic + héritage.

Tu ne peux pas avoir fait cela en python, du moins pas au sens des génériques tels qu'introduis dans golang, car ils n'ont de sens que dans un langage à typage statique (ce qui n'est pas le cas de python).

La fonctionnalité dont on parle consiste à rajouter aux langages des paramètres de types pour les fonctions. De même qu'avant, comme dans tout langage statiquement typé, il y avait des paramètres pour les valeurs contraintes par des types, il y a maintenant des paramètres de types contraints par des interfaces (paramètres de types qui pourront contraindre les paramètres de valeurs). Ce qui permet de lier, génériquement (c'est-à-dire indépendamment du type réellement instancié lors de l'appel de la fonction), les types d'entrée et de sortie des fonctions. Cela permet simplement d'appliquer le principe DRY (Don't Repeat Yourself), et je ne vois pas comment tu peux effectuer cela avec de simples clôtures.

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

Ça insiste quand même beaucoup sur son aspect de leader et sur le comportement ou les idées et non sur sa personne même.

Effectivement, cela insiste beaucoup sur son aspect de leader car c'est son retour au board de la FSF qui a mis le feu aux poudres. Cela étant, je continue tout de même à interpréter le « there is no space » par un « il n'y a aucune place », quelle qu'elle soit, et donc en particulier et à plus forte raison celle de direction et de représentation.

Mais entend moi bien, je ne suis pas particulièrement un fan de RMS, je trouve juste le texte de la pétition bien trop agressif et sans fondement sérieux contre lui. Sérieusement, les idées en question sont tout de même celles-ci :

He has shown himself to be misogynist, ableist, and transphobic, among other serious accusations of impropriety.

RMS serait donc misogyne, validiste et transphobe ? Il faut interpréter ses propos étrangement pour porter de telles accusations contre lui.

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

Le but est bien qu'il quitte des fonctions liées à la direction ou à la gestion d'un projet lié au Logiciel Libre, pas qu'il disparaisse entièrement.

J'ai comme un doute sur ton interprétation du document. Dans le paragraphe précédent, on trouve tout de même ceci :

Our communities have no space for people like Richard M. Stallman, and we will not continue suffering his behavior, giving him a leadership role, or otherwise holding him and his hurtful and dangerous ideology as acceptable.

Personnellement, j'interprète cela comme un bannissement complet de RMS de « nos communautés » et pas seulement de toutes fonctions de direction et de représentation (il n'y a pas de place, quelle qu'elle soit, pour des personnes comme lui).

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

Commence par la grammaire déjà.

Dit la personne qui, corrigeant deux petites erreurs de grammaire, trouve le moyen d'en faire une également.

Il se trouve que le groupe nominal sujet des deux verbes corrigés n'est autre que « l'ensemble de la population », groupe qui est un singulier du genre masculin. En conséquence, si la correction sur le verbe pouvoir est bien exacte, le participe passé ne nécessite nullement la marque du féminin. ;-)

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

Il y a aussi la pierre d'alun, bien connue des barbus conservateurs qui se rasent encore au coupe-choux. :-D

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

Combien de labos en fr_fr souffrent du manque de moyens pendant que depuis 50 ans le cea gâche les milliards par centaine ?

Je m'inscris en faux contre cette affirmation : ils ont la pierre philosophale ! En bombardant du mercure pendant un an dans un accélérateur de particules, on peut produire une pépite d'or en retranchant un proton aux atomes de mercure (cf. cette vidéo à 23:49). On peut certes douter de la rentabilité financière de l'opération. :-D

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

la solution serait d’envoyer un premier messager qui gueule un peu moins fort. :D

Je ne voudrais pas leur jeter la pierre, mais cela reste une idée bien saugrenue que d'avoir envoyé zenitram en éclaireur. :-D

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

Ce n'est pas parce que les patients qui partent en réanimation sont envoyés dans un autre service du CHU et que le service en question ne dépend pas de l'IHU

Ils ne sont pas envoyés dans un autre service mais dans un autre hôpital de l'AP-HM (Assistance Publique des Hôpitaux de Marseille), et ne sont donc pas comptabilisés dans les cas de décès de l'IHU. Les seuls décès de l'IHU sont les personnes trop agées ou grabataires et alors des soins palliatifs leur sont donnés à l'IHU jusqu'au décès.

(source).

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

Alors essayer d'en déduire les formalisme tout en étant préscriptiviste. C'est vouloir en faire des langues formelles.

Mais ce n'est pas du tout ce que je prône, ni ce qu'à jamais prôné la logique. Je ne vois pas où tu veux en venir, ni ce qui pu laisser entendre cela dans mes commentaires. Quoi qu'il y a bien, dans le passé (voire le présent), des logiciens avec une telle ambition mais ils étaient anti-kantien affichés. Donc, je ne vois pas comment je peux être associer à de telles personnes.

La première chose à faire, si on cherche à comprendre c'est de se débarrasser de ses apriori, accepter que ce que l'on prend pour acquis peut être remis en cause. Si ta question c'est "Pourquoi est-ce qu'ils se trompent ?", tu ne trouvera pas grand monde pour t'aider à trouver une réponse. De temps en temps des gens viendront essayer de dialoguer, mais ça va vite tourner en rond.

Ma question, sur le cas présent, n'était pas spécialement « pourquoi ils se trompent ? », mais pourquoi alors que Colin Pitrat se pose une question que tout homme peut se poser, on lui répond que sa question a une réponse qui n'en est pas une. Et le fait que la réponse n'en est pas une, il l'explicite on ne peut plus clairement dans son commentaire. La seule chose que que j'ai fait, c'est creuser un peu plus la question.

Enfin, je suis loin d'être le dernier à accepter que ce que je prends pour acquis puisse être remis en cause : c'est bien la base de la science après tout. Mais, enfin, quand on se place sur ce terrain là, il vaut mieux avoir du répondant, sinon on se retrouve sur facebook, tweeter ou youtube à avoir des gens qui t'expliquent que le coronavirus est un complot et que le masque est inutile. Et là, effectivement, toute discussion ou dispute (lorsqu'il y a débat) est vouée à l'échec. Mais j'ai bien trop de respect tant pour anaseto que pour toi, depuis le temps que je fréquente ces lieux, pour vous ranger dans ces cases là.

Après tout, il se peut que je me sois emporté parce que c'est un sujet (sur le plan scientifique¹, et donc de la rigueur intellectuelle) qui me tient particulièrement à cœur, mais je ne vois pas où j'ai dérapé. Si tu pouvais me l'indiquer (toi ou anaseto), je vous en serais reconnaissant.

Il est systématique dans chacun de tous tes commentaires. Quand tu ne cite pas nommément quelqu'un c'est 2500 ans d'histoires qui sont là pour appuyer ce que tu dis.

Mais parce que la science ne s'est pas faite en un jour. On ne peut pas aborder la savoir en partant du principe que rien ne s'est fait avant nous. Rien que ce qui a donné, par attaque et défense successive, l'informatique prend une partie de ses racines dans la philosophie kantienne et son désaccord avec Leibnitz sur certains points. Voir par exemple cet article de 1905 d'Henri Poicaré, là où il doute de l'espoir de Hilbert qui sera, justement, réduit à néant par Turing 30 ans plus tard. Comment veux-tu que je fasse comme si tout ceci n'avait pas exister ? Dois-je considérer que l'ordinateur est tombé du ciel du jour au lendemain ?

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

De ce qu'il me semble la logique s'intéresse uniquement aux langues formelles et à l'aspect objectif. Ce n'est qu'une petite partie du langage.

La logique ne s'intéresse pas, et à aucun moment, uniquement aux langues formelles. Elle s'intéresse à ce qu'il y a de formel dans toute langue (que celle-ci soit naturelle ou artificielle), ce qui constitue bien un aspect objectif du langage. Que ce ne soit qu'une partie, voire même une toute petite partie, de ce qui constitue un langage, je ne l'ai jamais nié et ne le nierai jamais. Ce n'est pas pour autant que c'est une partie à négliger.

Pour ce qui est de la nature de l'analyse logique et des langages dont elles s'occupent, tu pourras, par exemple, te reporter à mon analyse grammaticale du groupe adverbiale dans la langue française. Cela à commencer dans un journal sur la manière d'automatiser la punition consistant à recopier 100 fois la phrase « je ne dois pas jeter d'avion en papier en classe ». La précision « 100 fois » constituant le groupe adverbial (lui-même constitué d'un noyau et d'un complément), c'est-à-dire une précision, ou une spécification, de ce que le verbe « copier » signifie dans une telle phrase. Le début de l'analyse se trouve ici dans le journal à l'origine de la discussion, puis est développée plus en profondeur dans cette dépêche. Tout ce que j'ai écrit à l'époque relève de l'analyse logique du langage, bien que le support sur lequel elle s'exerce soit du français on ne peut plus usuel.

C'est justement parce que l'analyse logique s'applique à tout langage existant qu'elle se permet de prescrire des règles à ceux qui prétendent en inventer de toutes pièces. Libre à chacun de faire fie de ce qu'une science vielle de plus de 2500 ans affirme, mais il faut, dans ce cas, s'attendre à des retours de bâtons ;-)

Le fait d'être prescriptif c'est une branche de la logique, mais je pense que ça capture bien ce que je trouve profondément gênant avec tes messages.

Le fait d'être prescriptif n'est nullement une branche mais l'essence même de la logique, je ne vois pas à quoi elle pourrait servir d'autre. J'entends bien que tu trouves cela gênant dans mes messages, mais je te rétorque la question : pourquoi ? Dans une autre discussion, tu en es venu à parler d'Einstein et de sa théorie de la gravitation, en expliquant, à bon droit, que ce n'est pas parce qu'une personne avait observé toute sa vie des objets tombés qu'elles comprenait la théorie de la relativité générale. Ceci étant, considérerait-on comme acceptable qu'une personne voulant construire un système de GPS se permette d'ignorer cette théorie et donc l'influence du champ de gravitation sur la marche des horloges (comment synchroniser l'horloge du satellite et celle du récepteur resté sur terre ?) ?

À titre personnel, ce que je trouve gênant est qu'il existe une science vielle de plus de 2500 ans dont certains programmeurs (en particulier certains concepteurs de langages) semblent se moquer. J'entends par « se moquer » non se rire d'elle, mais être indifférent à ce qu'elle prescrit. Et j'ai beau retourner la question dans tous les sens dans ma tête, je n'en comprends pas la raison. Mon appel aux philosophes (je ne vois pas en quoi il a été continuel) n'étant là que pour rappeler cet état de fait : les questions ne datent pas d'aujourd'hui mais ont des siècles de réflexions humaines derrière elles.

À la base tout est partie d'une question, on ne peut plus naturelle, à savoir : comme, de deux chose l'une, un appel de fonction peut réussir ou échouer, pourquoi ne pas répondre par une alternative comme le fait Rust ? Sur cela, comme il s'agit de faire usage d'un type somme¹, j'ai généralisé la question : pourquoi Go n'a pas de type somme ? Sur ces entrefaits les réponses qui m'ont été apporté ne m'ont pas convaincues, si ce n'est que les utilisateurs ou responsables du langages (cf la PR mise en lien par anaseto) ne maîtrisaient pas les notions dont il était question.

Je n'ai jamais eu, et n'aurais jamais, la volonté d'étaler ma science en place publique. C'est là une attitude que je trouve soit indécente, soit puérile. En revanche, quand je demande à ce que l'on me montre un chat, puis que l'on me montre un animal qui certes, est un quadrupède, à une queue, des poils… mais qui, quand que je joue avec, se met à aboyer, je réponds que j'ai affaire à un chien et non à un chat.

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

Lorsque tu expliques que pour toi le système de types de Go est un « jouet playskool que l'on donne aux enfants », tu ne dis pas que c'est en comparaison du super jouet bien plus fun qu'est le système de types OCaml. Du coup, quelqu'un qui n'a pas une bonne connaissance de l'historique de tes messages va prendre cela dans le sens que le système de types de Go est un jouet à côté de celui de OCaml

Il y a une chose que je ne suis pas dans ce passage de ton commentaire : l'interprétation qu'une personne sans connaissance de l'historique de mes messages est tout à fait correct. Ce système de types est un jouet pour enfant à côté de celui d'OCaml. Je comprends que cela puisse être désagréable à lire, mais c'est bien ce que je pense. Là, c'est le logicien en moi qui s'exprime.

Là logique est une science dont l'objet d'étude est, comme son nom l'indique, le langage. Mais elle ne l'étudie pas à la manière de la linguistique, c'est-à-dire qu'elle ne s'intéresse pas à telle ou telle langues données pour les analyser comparativement dans leurs structures. Si je peut m'exprimer ainsi, ce qu'elle cherche à travers la diversité des langues c'est les invariants par variations. Elle cherche les lois nécessaires de toute pensée, dont le langage n'est que le moyen d'expression. En conséquence, elle n'a pas une approche descriptive comme la linguistique, mais une approche prescriptive et, comme le disait Kant dans le traité qu'il lui a consacré :

La logique est une science rationnelle non seulement selon la forme, mais selon la matière; une science a priori des lois nécessaires de la pensée, non pas relativement à des objets particuliers, mais bien relativement à tous les objets en général; c'est donc une science du droit usage de l'entendement et de la raison en général, non pas de façon subjective, c'est-à-dire selon des principes empiriques (psychologique) : comment l'entendement pense — mais de façon objective, c'est-à-dire selon des principes a priori : comment il doit penser.

Kant, logique.

L'aspect prescriptif se trouve à la fin de la définition qu'il donne de cette science : « comment il doit penser ».

Ensuite, ce que la logique a à apporter à la programmation et à ses langages, ce n'est pas ce calcul assez simple sur les booléens, mais la théorie des types. Les notions centrales de la logique sont celles de concepts, jugement et raisonnement. Par miroir, ces notions en informatique sont celle de types, jugements de typage et dérivation de typage.

Résultat, quand je regarde le système de type de Go, j'ai une logique tellement amputée de certains de ses concepts et principes, que l'ensemble m'apparaît réellement comme un jouet : la logique sous-jacente est simpliste en comparaison de ce que contient la logique. Ce qui n'est absolument pas le cas avec le système de types d'OCaml (ou Haskell). Ce qui est amusant, au passage, c'est qu'il y a une implémentation de ce systèmes en Go : le cœur du langage c'est le système F et celui-ci constitue le langage de configuration Dhall.

Par exemple, ce qui me manque, en premier, c'est l'absence de jugement disjonctif : la totalité de ce dont nous débattons depuis le début (et même avant que j'intervienne sur ce fil de discussion). La disjonction n'est pas une opération qui prend deux booléens puis en retourne un troisième, mais une opération qui prend deux jugements puis en produit un troisième. La première opération apparait lorsque l'on interprète ces jugements selon leur valeur de vérité, et cette notion n'est pas primitive mais dérivée.

Les jugements disjonctifs donne naissance aux types somme (A ou B), là où les jugements conjonctifs donnent naissance aux types produit comme les struct (A et B). Les premiers sont fait pour être utiliser ainsi :

Le caractère propre de tous les jugements disjonctifs, qui détermine, au point de vue de la relation, leur différence spécifique relativement aux autres et particulièrement aux jugements catégoriques, consiste en ce que les membres de la disjonction sont en totalité des jugements problématiques, dont ne peut rien penser d'autre que ceci : étant les parties de la sphère d'une connaissance, chacun complétant l'autre pour former le tout (complementum ad totum), pris ensemble, ils équivalent à la sphère du tout. Il s'ensuit que la vérité doit être contenue dans l'un des jugements problématiques, ou, ce qui revient au même, que l'un d'eux doit avoir valeur assertotique, puisqu'en dehors d'eux, la sphère de la connaissance n'englobe rien sous les conditions données et qu'ils sont opposés les uns aux autres; par suite il n'est possible ni qu'il y ait en dehors un autre jugement qui soit vrai, ni qu'il y en ait plus d'un parmi eux.

Kant, logique.

Afin d'avoir ce qu'exige l'usage logique des jugements disjonctifs (« il n'est possible ni qu'il y ait en dehors un autre jugement qui soit vrai, ni qu'il y en ait plus d'un parmi eux »), il est nécessaire que le langage, via son système de types, fournisse de manière primitive les sommes fermées, puis qu'il vérifie l'exhaustivité de leur usage.

Dans le reste, on peut aussi lui reprocher de ne pas pouvoir faire abstraction des jugements, c'est-à-dire pas de variables de types ou généricité. Il n'y a pas de sous-typage, le cœur de la syllogistique aristotélicienne : tous les animaux sont mortels, tous les hommes sont des animaux, donc tous les hommes sont mortels.¹ L'usage des raisonnements hypothétique (si A alors B) est bien présent au niveau des booléens (if then else) mais ne semble pas être mis si en avant que cela, et moins évident à utiliser qu'OCaml, au niveau des types (ici c'est le type des fonction, comme f : int -> float).

Je devrais sans doute pouvoir trouver d'autres choses qui me manquent en creusant un peu le langage, mais cela fait déjà beaucoup trop à mon goût. Autant d'absences qui peuvent difficilement me le faire considérer autrement que comme un jouet, relativement à ce que je chercherais à faire avec, quand bien même cette expression pourrait paraître déplaisante à ces utilisateurs.

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

En C++, l'explosion de code provenait de la création d'une nouvelle fonction à chaque usage d'une fonction générique.

Ça c'est parce que C++ pratique la monomorphisation afin de spécifier chaque instance de template et avoir un code plus efficace. Cela se fait au prix d'une multiplication du nombre de fonctions pour chaque instance d'une template. C'est un choix de stratégie de compilation : les template sont instanciés à la compilation, là où un foncteur OCaml ne génère qu'une fonction et est instancié à l'exécution (une fois compilé un module n'est rien d'autre qu'un enregistrement comme les autres, tous les types étant effacés à la compilation, et un foncteur un fonction générique qui crée un enregistrement à partir d'un autre enregistrement).

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

Mais si je ne connaissais pas OCaml, je pourrais naïvement croire que le système de types de Go est clairement mauvais et croire aux allégations mal informées d'ignorance académique de ses créateurs ou autre : oui, ils ne sont pas des chercheurs en systèmes de types avancés, mais un langage de programmation ne se limite pas à ça.

Je n'ai pas dit que leur système de types est mauvais (ce que tu développes et défend, je l'avais fait à l'époque du journal de gasche que j'ai cité plus haut) mais qu'il n'était pas assez sérieux pour ce que j'aime faire. Tu ne peux pas dire objectivement que les deux systèmes de types de OCaml et de Go sont du même niveau. J'exprime donc une opinion personnelle relative à mes besoins.

Quand tu répètes en boucle que tu apprécies la réflexion pour ses capacités de marshalling, je ne nie pas la chose, ni interdit à toi ou d'autres développeurs d'avoir ce besoin. En revanche, je me permets de répondre que le fait que ce soit intégré de base dans le langage ne m'intéresse pas. J'ai pas le droit d'avoir des goûts distincts des tiens ?

Par contre lorsque tu affirmes que vous avez des types somme, je me permet de le nier objectivement. Que tu veuilles entendre ou non raison m'indiffère, mais la chose n'en reste pas moins vraie. Tu peux tout à fait reconnaître que tu n'en vois pas l'intérêt, et que cela ne te manque pas plus que cela, mais je n'appellerais jamais type somme ce dont vous disposez, tout comme je n'appellerai pas types dépendants ce que l'on fait en OCaml avec des types fantômes.

Pour revenir sur les goûts personnels, je reconnais volontiers qu'un langage ne se limite pas à un système de types, mais je ne suis pas programmeur, et la seule chose qui m'intéresse dans un langage c'est de jouer avec ses types. Avec Go je m'ennuierai vite, avec OCaml je m'amuse : c'est tout ce que je voulais dire par système de types plus sérieux. Tout comme j'adore son système de modules et me moque totalement qu'il soit ou non facilement accessible : je suis mathématicien et logicien de formation et le discours mathématiques est structuré selon le système de modules OCaml depuis Euclide jusqu'à nos jours, je navigue là dedans comme un poisson dans l'eau. Par exemples les concepts de bases de l'algèbre linéaire sont des types de modules :

module type Groupe = sig
 type t (* le type du support du groupe *)
 val zero : t (*l'élément neutre *)
 val add : t -> t -> t (* l'opération binaire sur t *)
 val neg : t -> t (* tout élément a un oppposé *)
end

(* un corps est un groupe muni d'une opération inversible
   et distributive sur l'addition *)
module type Corps = sig
  include Groupe
  val one : t (* élément neutre pour la multiplication *)
  val mul : t -> t -> t (* la multiplication *)
  val inv : t -> t (* inverse pour la multiplication *)
end

(* Enfin un espace vectoriel est la donné d'un groupe, dont les
   éléments sont appelés vecteurs, puis d'un corps dont les éléments
   sont appelé scalaires, ainsi que d'un produit extérieur des scalaires
   sur les vecteurs, aussi appelé `scale` en anglais *)
module Espace_vectoriel = sig
  module V : Groupe
  module K : Corps
  type vector = V.t
  type scalar = K.t
  val scale : scalar -> vector -> vector
end

La seule chose que je regrette étant que le système ne soit pas assez intégré dans le cœur du langage (c'est un langage à part, OCaml c'est deux langages en un), de telle sorte que l'on ne peut pas manipuler vraiment les modules comme des objets de première classe, mais cela évolue dans le bon sens. Avec le systèmes des interfaces, je resentirai un manque dans ma capacité d'expression. D'ailleurs le système est plus puissant que le système des types classes de Haskell, et lorsque Simon Peyton Jones (principal contributeur au compilateur GHC de Haskell) a soutenu le contraire, je me suis permis de le corriger. Ce n'est donc pas ton insistance à affirmer que Go a des types somme qui m'arrêtera.

Enfin concernant l'ignorance académique sur les systèmes de types, j'aimerai me tromper mais c'est vraiment ce que j'ai ressenti à la lecture en diagonale de la PR sur les types somme dont tu as donné le lien. Tu pensais, je te cite, que « mon impression, c'est que tu ne sembles pas saisir les subtilités des interfaces Go » alors qu'il m'a fallu moins de dix minutes de réflexion pour en comprendre la formalisation à partir de ta description. Ce fût plus long pour te convaincre que tel était le cas : relis bien tous mes commentaires.

Pour conclure sur la notion d'abstraction :

On n'emploie pas toujours correctement en logique le terme : abstraction. Nous ne devons pas dire : abstraire quelque chose (abstrahere aliquid), mais abstraire de quelque chose (abstrahere ab aliquo). Si par exemple dans un drap écarlate je pense uniquement au rouge, je fais abstraction du drap; si je fais en outre abstraction de ce dernier en mettant à penser l'écarlate comme une substance matérielle en général, je fais abstraction d'encore plus de déterminations, et mon concept est devenu par là encore plus abstrait. Car plus on écarte d'un concept de caractères distinctifs des choses, c'est-à-dire plus on en abstrait de déterminations, plus le concept est abstrait. C'est donc abstrayants (conceptus abstrahentes) qu'on devrait nommer les concepts abstraits, c'est-à-dire ceux dans lesquels d'avantage d'abstractions ont eu lieu. Ainsi par exemple, le concept de corps n'est pas à proprement parler un concept abstrait; car du corps lui-même je ne puis faire abstraction puisque dans ce cas je n'en aurais pas le concept. Mais il faut bien que je fasse abstraction de la taille, de la couleur, de la dureté ou de la fluidité, bref de tous les déterminations spéciales des corps particuliers — Le concept le plus abstrait est celui qui n'a rien de commun avec ce qui diffèrent de lui. C'est le concept de quelque chose; car le concept qui s'en distingue est celui de rien et il n'a donc rien de commun avec le quelque chose.

Kant, Logique.

Votre type interface {}, c'est cela, le concept le plus abstrait, celui de quelque chose : il n'y a plus rien à abstraire, l'ensemble des méthodes étant vide. Raison pour laquelle tu as dis que si tu l'avais choisi au lieu des int tu aurais eu des listes hétérogènes de choses à la python. Comme cela, une liste de choses :

[Top(Int, 1); Top(List Int, [0; 1; 2]); Top(Float, 3.5)];;
- : top list = [Top (Int, <poly>); Top (List Int, <poly>); Top (Float, <poly>)]

Ce qui montre que le type top pourrait s'appeler anything (enfin ce n'est pas tout à fait celui-ci le type anything en OCaml mais type any = Any : 'a -> any). Et les concepts c'est la base de la pensée : plus je peux en définir, plus je peux exprimer convenablement ma pensée. Mais un type, en informatique, n'étant rien d'autre qu'un concept… Ou l'on voit d'ailleurs que, déjà en français, la notion de listes s'exprime sous la forme d'un type paramétrique (généricité quand tu nous tiens ;-) : le complément du nom dans les expressions liste d'entiers, liste de course, liste de noms ou liste de choses est lui même un concept, c'est-à-dire un type. ;-)

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

Je peux comprendre que tu ne perçoives pas l'intérêt de la proposition expérimentale de gasche, mais le but du lien était de te montrer que les power users des types somme ressentent le besoin de travailler sur les patterns et motifs de destruction, que cela fait partie intégrante de l'usage des types sommes. Un type somme ne peut s'utiliser autrement que par déstructuration de son motif.

Si tu veux un exemple moins alambiqué et bien plus courant, regarde celui de la fonction simplify_first_col dans ce journal de gasche. Ou celui-ci :

type A | B

match v with
|Ok A -> ...
|Ok B -> ...
|Error _ -> ...

(* comparé à *)

match v with
| Ok v -> match v with A -> ... | B -> ...
| Error _ -> ...

Quand on fait une somme de somme, extrêmement courant dans un langage disposant nativement et naturellement de types somme, on aime bien aplatir la somme dans la destruction de motif.

Et puis tu compares un différence de verbosité (encodage verbeux des types somme en Go), voire d'expressivité du typage (distinction somme ouverte ou fermée conduisant à des warnings utiles), à une différence d'expressivité du langage (définir une fonction d'affichage qui donnera un affichage par défaut pour les types créés par n'importe quel utilisateur).

Alors premièrement la distinction somme ouverte ou fermée est de la plus haute importance ! Cela va bien au-delà de l'existence de warnings utiles, il s'agit de savoir de quoi l'on parle. Une somme ouverte est plus ou moins improprement appelé une somme. Elle ne désigne pas un seul type précis mais une famille illimitée de types : faire passer l'un pour l'autre s'est se moquer du monde. Je me souviens d'avoir vu reprocher en ces lieux que les philosophes ne définissaient pas ou mal leurs concepts, ce qui m'avait fait sourire, mais à côté des programmeurs ils sont la rigueur incarnée en comparaison.

Une somme de deux types c'est le plus petit des majorants (à isomorphisme près) par la relation de sous-typage, une somme ouverte les contenant c'est un majorant quelconque ! Je te donne deux entiers, disons 2 et 3, et si je te dis que 36 est leur plus petit commun multiple tu ne tiques pas ? C'est exactement ce que tu fais en voulant éluder la distinction entre somme ouverte et fermée. Le produit étant la version duale c'est à dire les plus grand des minorants, ou le pgcd pour l'analogue chez les entiers.

Donc non, c'est clair, vous n'avez pas la somme de deux types en Go, jusqu'à preuve du contraire. Ou si vous l'aviez, il faudra m'expliquer la raison étrange d'avoir choisi le produit, et non la somme, comme convention pour vos fonctions pouvant retourner une erreur (ce qui est le point de départ de toute cette discussion).

Je le répète et j'insiste profondément : tu n'as pas encodé la somme de deux types. Ce point là, je ne te l'accorderais jamais. Par comparaison, on mimique en OCaml avec des types fantomes ce qui en réalité relève des types dépendants : le concept de fichier en lecture seul est un type dépendant. Et pourtant aucun développeur OCaml n'irait soutenir que l'on a des types dépendants en OCaml (voir cette interview de Leo White).

Ensuite mon illustration sur le type top et la fonction qui en fait usage avait pour but de t'expliquer, avec du code, ce que gasche t'avait déjà expliqué en 2017. Et pour ceux de ta communauté (voir la PR sur les type somme) qui craignent un problème d'interaction entre type somme et interface {}, ils ne se passe rien, tout va bien :

Ok (Top(Int, 1));;
- : (top, 'a) result = Ok (Top (Int, <poly>))

Pour ce qui est de la fonction d'affichage générique, c'est une question de goût : je n'en ai rien à faire. Pour être franc et honnête, le système de types de Go est pour moi de l'ordre du jouer playskool que l'on donne aux enfants, je n'irais pas utiliser une telle chose juste pour disposer d'une telle fonction : j'ai des ppx pour cela, elles dérivent un formateur pour les types définis par l'utilisateur et utilisables avec la chaîne de formatage "%a" (l'équivalent de ton "+%v").

Format.printf "%a" Format.pp_print_int 1;;
1- : unit = ()

Les extensions de syntaxes ppx dérivent un pretty printer (pp) à utiliser comme celui fournit par défaut pour les int. Ce qui revient tout à fait au même que votre printf en Go, mais avec un système de types un peu plus sérieux.

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

Je me demande quels types d'applications tu as en tête, pour que le côté récursif en profondeur de la destructuration te semble à ce point indispensable.

Regarde par exemple ce fil de discussion ouvert par Gasche sur le forum OCaml : Musings on extended pattern-matching syntaxes. Tu verras à quel point le pattern matching est essentiel dans l'utilisation poussée des types sommes. Quand on a des types sommes un peu partout, on déstructure à tous les niveaux et tout le temps.

Je t'accorde que la différence est syntaxique, et ne concerne pas le système de types, mais elle est essentielle pour l'usage convenable de types sommes. Déjà qu'ils sont une plaie à définir en Go, qu'ils sont ouverts et non fermés, si en plus on n'a aucune construction syntaxique aidant à leur usage, ce qui est clair et net c'est que ce n'est absolument pas une alternative viable aux types sommes.

Quand je t'ai montré comment faire de la réflexion avec des GADT en OCaml, tu m'as répondu cela :

Ce n'est pas une petite différence ! Surtout que le « à la main » passe par le concept de GADT, qui n'est pas le plus accessible

Et après tu me présentes les interfaces comme alternatives crédibles aux types sommes, via ton encodage du dessus. Tu es à la limite de la mauvaise foi sur le coup.

Je veux bien t'accorder que le concept de GADT, si on veut en explorer tout le potentiel, est difficile d'accès. Mais le cas d'usage que je proposais est utilisable par n'importe qui, sans avoir besoin de saisir les subtilités qu'il y a derrière. Je redonne sa définition :

type _ ty = ..

type _ ty +=
  | Int : int ty
  | Float : float ty
  | List : 'a ty -> 'a list ty

Sans rien comprendre à ce qui passe derrière, lorsque l'on définit un nouveau type, disons celui-ci :

type moule = {pseudo : string; karma : int}

il suffit de faire avec :

type _ ty += Moule : moule ty

c'est-à-dire rajouter un constructeur constant qui à le nom du type puis lui donné le bon type. Ce n'est certainement pas plus compliqué que ton encodage de types somme ouverts. Et au fond, votre type interface {} ce n'est rien d'autre que celui-ci emballé dans un type existentiel :

type top = Top : 'a ty * 'a -> top

Exemple de code qui prend une interface {} et fait un switch sur type :

let f (Top (t, v)) = match t with
  | Int -> Format.printf "%d@." v
  | Float -> Format.printf "%f@." v
  | _ -> ()

(* et à l'usage *)
f (Top(Int, 1));;
1
- : unit = ()

f (Top(Float, 2.5));;
2.500000
- : unit = ()

Ce qui revient à ce que je disais depuis le début : vous avez un type somme extensible gérer par le compilateur pour chaque interface, qu'il enveloppe dans une type existentiel. Comme je l'ai fait : j'ai emballé le GADT extensible dans un couple (type, valeur) puis je fait du pattern matching sur des constantes : ce à quoi se résume ton encodage des types sommes en Go.

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

Je vais plutôt donner un réponse générale à ton commentaire qui, malheureusement, confirme ma position initiale : le système des interfaces n'est pas une alternative viable aux types sommes.

Premièrement, ta solution d'interface IntOrString ne répond pas pleinement au problème. La somme est ouverte et non fermée, j'ai pu y rajouter un float64 avec ce code :

type C float64
func (c C) ImplementsIntOrString() {}

Le point positif, si on passe un valeur de type C à une fonction qui attend uniquement un A ou un B, est que tout se passe bien. J'ai testé avec une fonction d'affichage (qui alors n'affiche rien), mais si elle devait retourner une valeur je suppose qu'elle retournerait la valeur par défaut de son type de retour (il me semble que chaque type a une valeur par défaut).

Néanmoins, le filtrage par motif n'est pas qu'une affaire de syntaxe : c'est un élément crucial dans l'utilisation des types sommes, sans cela ils perdent tout de leur intérêt. Mon point n'était pas tant de savoir si l'on pouvait encoder des types sommes avec les interfaces, mais de savoir s'ils satisfont cette requête :

C'est pas étonnant qu'ils soient absents, puisque la pratique de programmation qu'ils couvrent est déjà couverte par le concept des interfaces (bien que ce ne soient pas des type somme implémentés de façon scolaire).

J'ai cité un extrait d'un de tes commentaires précédents. Sans le filtrage par motifs, ils ne couvrent absolument par la pratique de programmation des types sommes. En revanche, sous le capot, ils sont bien implémentés sous la forme d'un type somme extensible, comme celui que j'avais utilisé pour la réflexion. C'est là un choix d'implémentation pour la fonctionnalité du polymorphisme ad hoc.

Il y a eu deux propositions pour ajouter cette fonctionnalité à OCaml : une basée sur une implémentation à la Go utilisant le type pour la réflexion et une autre basée sur le système de modules et foncteurs à la type classes de Haskell. C'est la dernière qui a était retenue et qui est en cours d'élaboration, mais qui demande encore des travaux de recherches pour faire cela proprement au niveau du système de types.

Quoi qu'il en soit, merci pour cette échange qui m'a permis de comprendre un peu mieux la manière dont les interfaces sont implémentées dans ce langage.

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

L'utilisation de Printf dans l'exemple que j'ai donné l'illustre bien : rien n'a été fait pour permettre l'affichage des nouveaux types.

Je viens de faire un test avec votre version de Printf. Cela doit être une question de point de vue, mais pour moi elle est moisie.

fmt.Printf("%d", 1) // Imprime bien 1

fmt.Printf("%d", "hello") // Imprime "%!d(string=hello)"

Le deuxième exemple ne devrait pas compiler! Si je dois abandonner la sécurité du typage statique parce qu'il y a des programmeurs pas capable de définir leur formateur pour les types qu'ils définissent, je préfère rester avec ce que j'ai. ;-)

Format.printf "%i" 1;;
1- : unit = ()

Format.printf "%i" "hello";;
Line 1, characters 19-26:
Error: This expression has type string but an expression was expected of type
         int

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

Mon impression, c'est que tu ne sembles pas saisir les subtilités des interfaces Go partant de préjugés sur le sens du mot « interface »

C'est pas un préjugé sur le mot « interface », c'est ainsi que le concept est présenté dans A Tour of Go.

Et je dois dire que j'ai toujours du mal à voir en quoi, avec tous les exemples que tu me donnes, cela peut être considérer comme fournissant une fonctionnalité équivalente aux types sommes. Si c'est le cas tu dois bien pouvoir me définir simplement la somme de deux types, disons int et string, de telles sortes que le type ainsi défini ne puisse contenir que des valeurs de l'un ou de l'autre (union ensembliste) et rien que celles-là.

Autrement dit, tu dois pouvoir me définir cela (je l'espère sans encodage tricky) :

type int_or_string = A of int | B of string

À partir de ton type de liste de int, tu devrais pouvoir définir trivialement cette version de la fonction last calculant le dernier élément de la liste :

let rec last = function
  | [] -> None
  | [x] | [_; x] | [_; _; x] -> Some x
  | _ :: _ :: _ :: l -> last l

Quand je dis cette version, c'est celle avec 5 switchs. C'est équivalent au déroulement d'une boucle. Partant du type list A = 1 + A + A^2 + A^3 + A^4 +..., j'ai un switch pour les puissances 0, 1, 2 et 3 puis un dernier pour toute puissance ≥ 4.

je peux représenter tout type somme comme la disjonction des types satisfaisant une interface.

Comme peux tu limiter, à priori, les membres de cette disjonction ? Qui te dit qu'un utilisateur, sur lequel tu n'as aucun contrôle, ne créera pas un type satisfaisant l'interface en question ?

Tant que je n'aurais pas une solution, claire et nette, à ces problèmes, je ne considérerais pas les interfaces comme un substitut aux types sommes. Même pas de loin, en tant que version du pauvre.

Lors d'un type switch il n'y a pas de typage dynamique : toutes les variables sont typés statiquement dans chaque branche, comme lors d'un filtrage par motif d'un type somme.

Quand je parlais de typage dynamique, je faisais allusion au type interface{}. C'est le type top (celui qui contient tout valeur, qui est le plus grand de tous les types par la relation de sous-typage), et un type switch sur une telle valeur ressemble fortement à du rafinement de type dynamique (même si le type est connu statiquement dans chaque branche). Un langage à typage dynamique, comme Python, est un langage avec un seul type statique à savoir top. C'était pour parler de votre gestion du Printf, qui est appelé sur cette interface.

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

C'est pas étonnant qu'ils soient absents, puisque la pratique de programmation qu'ils couvrent est déjà couverte par le concept des interfaces

Absolument pas, et ton exemple sur les listes chaînées me le prouvent une fois de plus. Mais là on tourne en rond, et tu ne sembles vraiment pas saisir à quoi servent les type sommes (étonnant pour une personne ayant programmé en Rust, Haskell, OCaml et Coq).

Sauf que les conventions font qu'il n'y a pas 4 cas en pratique, mais bien 2 sauf 3 dans de rares cas comme Read qui peut renvoyer une erreur EOF qu'on peut vouloir traiter de façon particulière (cas non gérable par un simple type somme A + B de toutes façons).

Avec les types sommes ce serait plus qu'une convention, elle serait vérifiée statiquement par le type checker. Outre l'API étrange de renvoyer une erreur et une résultat en même temps, cela se fait très bien avec un type somme, même de la forme A + B. L'existence du troisième cas fait que la valeur de retour est de la forme A + B + A * B, ce qui, par de l'algèbre niveau collège, se ramène à une somme de deux termes A + B * (1 + A)

Pour le reste c'est lié à la réflection et au typage dynamique du langage, ce qui peut aussi se faire statiquement à base de prépocesseur comme en Haskell, Rust… ou OCaml. Et donc toute cette discussion est hors sujet par rapport à l'existence ou l'absence des types sommes.

Soit dit en passant, si l'on oublie de traiter un cas dans un type somme, le code compile et le compilateur émet un warning et non une erreur :

function [] -> 0;;
Line 1, characters 0-16:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
_::_
- : 'a list -> int = <fun>

Autrement dit cela fait exactement ce que tu attends (cf. une de tes réponses à Nicolas Boulay)

C'est très sympa, mais je pense personnellement que ce serait mieux sous la forme d'un warning ou d'une analyse statique : ça permet de trouver tous les endroits à modifier tout en permettant les modifications graduelles. Ça donnerait les avantages sans les inconvénients.

C'est exactement le comportement du compilateur face aux types sommes : warning et analyse statique.

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

C'est peut-être une vision tordue (pour le théoricien du typage), mais, dans les faits, c'est équivalent (au côté infini près) et simple à comprendre, même si ce n'est pas une implémentation exclusive des types somme directement calquée sur un papier de recherche.

Pas besoin d'un papier de recherche pour cela, la notion de type somme c'est du niveau licence en mathématiques : c'est la somme disjointe d'ensemble (définie par une disjonction exclusive) qui est la notion jumelle du produit cartésien (type produit défini par une conjonction). Il n'y a rien de hautement sophistiqué là-dedans. C'est bien pour cela que je m'étonne de leur absence.

D'ailleurs, outre cette représentation dynamique des types, vous avez d'autres types sommes dans le langage. Si j'ai bien compris, la valeur nil peut être affectée à n'importe quel type, ce qui fait qu'en réalité vous ne manipulez que des types options, qui est un type somme : c'est le type 1 + A pour tout type A. Ce qui fait que lorsque vous avez des fonctions qui peuvent retourner une erreur, en renvoyant une paire, vous retournez un type produit de la forme suivante : (1 + A) * (1 + B) = 1 + A + B + A*B, où l'on voit les 4 cas à gérer que déplorait Colin Pitrat dans son premier commentaire. Là où, avec un type somme de résultat, il n'y a que les deux cas A + B.

Et ce n'est pas équivalent, même dans les faits. Cela l'est tout autant que Platon définissant l'homme comme un bipède sans plumes, et Diogène le cynique de le rayer en se promenant avec un poulet déplumé tout en haranguant la foule d'un « Voici un homme ! ».

Il y a d'autres types sommes infinis que l'on ne peut définir, en tant que tel, avec Go : celui des listes par exemples. Un type somme récursif, comme celui des listes, se développe en une somme infinie : 1 + A + A^2 + A^3 + ..., c'est-à-dire la liste vide, ou les listes à un élément, ou les listes à deux éléments, ou les listes à trois éléments…

Tout ce que vous avez, c'est le type somme extensible que j'ai défini précédemment, qui est géré par le compilo et accolé dans une paire à toute valeur utilisant une interface. Puis vous faites du pattern matching dessus. Mais les seuls cas d'usage que j'ai vu, c'est avec l'interface vide pour palier le manque de polymorphisme dans le langage. L'exemple que tu m'as donné pour les arbres ne semble pas faire de d'analyse de cas sur la représentation dynamique des types, mais définir des arbres dans un langage qui n'a pas de type somme (directement définissables et accessibles au programmeur) mais que des types produits (ou struct ou enregistrements…) comme on peut le faire en C, C++, Java, Python, etc.

Ce n'est pas une petite différence ! Surtout que le « à la main » passe par le concept de GADT, qui n'est pas le plus accessible

Ce que je veux dire c'est que l'outillage est là pour avoir une représentation dynamique des types, et que ce que j'ai fait à la main le compilo pourrait le faire automatiquement. Ce n'est pas la partie la plus dure, seulement je ne crois pas que quelqu'un y ait vu un quelconque intérêt à l'implémenter.

je ne vois pas comment tu pourrais définir une fonction qui marche pour tout type (dont ceux définis ultérieurement par un utilisateur).

Je ne vois pas comment tu pourrais le faire aussi, simplement en bénéficiant d'un représentation dynamique des types. Soit la fonction est polymorphiquement paramétrique et là c'est très usuel en OCaml, soit le poylmorphisme est ad hoc et c'est le système des type classes (ou interface pour Go, mais le switch sur type ne sert à rien). Où a-t-on besoin d'une représentation dynamique des types ?

Par exemple, en Go on peut faire sans plus d'histoires un marshall et unmarshall (à l'aide du module encoding/gob) de presque n'importe quel type de façon type safe (en OCaml le module équivalent n'est pas type safe).

On peut faire de la sérialisation/déserialisation de manière type safe en OCaml, mais c'est ad hoc, il faut choisir son format. Les modules de la lib standard font cela de manière générique, ce qui ne peut être type safe. Même si l'on avait une représenation dynamique des types, je ne suis pas certain que l'on puisse réellement faire cela de manière générique et type safe.

Autre exemple : printf.

Pour faire un printf type safe il me semble qu'il faut les types dépendants, et en OCaml c'est implémenté via un GADT.

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

Non, pas vraiment : en Go les interfaces sont des valeurs à part entière assimilables à un couple (type, valeur) dont on peut inspecter chaque composant à l'exécution.

C'est l'implémentation de la fonctionnalité qui veut cela, mais ça n'a rien à voir avec la notion générale de type somme. La valeur (du couple) est un dictionnaire, c'est-à-dire un type produit. Quand vous utilisez une interface, vous affirmez l'existence unique d'un certain dictionnaire pour le type qui vous intéresse. Alors, effectivement, un énoncé qui quantifie existentiellement et de manière unique sur les types est équivalent à une disjonction exclusive infinie, mais c'est là une vision tordue de ce que sont réellement les types sommes.

Quand on dit qu'il existe un unique entier satisfaisant une propriété P, c'est tout comme si l'on disait cette disjonction exclusive infinie : P0 ou P1 ou P2 ou P3… Avec vos interfaces vous fait la même chose mais en quantifiant sur les types, puis vous examiner au runtime lequel des types implémente le dictionnaire. Mais c'est là un choix d'implémentation du mécanisme (c'est bien plus simple que de tout gérer à la compilation) qui dans le principe n'est rien d'autre que celui des arguments implicites de type produit. Vous auriez pu faire la même chose en vous contentant d'avoir une représentation du type au runtime et sans interface.

elle résout aussi la question de la réflection et ses applications intéressantes (en particulier en sérialisation) dont on ne profite ni en Rust, ni en OCaml ou Haskell

C'est tout à fait possible en OCaml avec les types GADT extensibles, mais je dois dire que je n'en ai jamais bien compris l'intérêt (c'est quoi ces fameuses applications intéressantes ?). À la différence qu'il faut se taper à la main ce que le compilateur Go fait automatiquement pour vous. Un GADT extensible permet de définir une somme illimitée de couple (type, valeur), ce qui est l'implémentation retenue pour les interfaces.

Exemples avec mon interface showable :

type _ ty = ..

type _ ty +=
  | Int : int ty
  | Float : float ty
  | List : 'a ty -> 'a list ty

let couple = (Int, {show = string_of_int});;
val couple : int ty * int showable = (Int, {show = <fun>})

(* on peut étendre le GADT *)
type _ ty += String : string ty

let couple2 = String, {show = fun s -> s};;
val couple2 : string ty * string showable = (String, {show = <fun>})

Voilà, ma valeur couple est une paire constituée d'une représentation au runtime du type int ainsi que d'un dictionnaire implémentant l'interface showable pour lui. Mais avec les type sommes extensibles, on perd la vérifications de l'exhaustivité lorsque l'on s'en sert. ;-)

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

en fait, les interfaces de Go (qui sont des valeurs) peuvent être (et au besoin sont) utilisées exactement comme les types somme à l'aide d'un type switch (le cas courant de l'énumération se fait d'habitude avec des constantes).

Cela peut certes être utilisé dans certain cas en lieu et place d'un type somme, mais ce n'est vraiment pas la même notion. Les interfaces, c'est les type classes de Haskell ou les traits de Rust, mais en version du pauvre. Les fonctions qui prennent un interface en paramètre c'est juste des fonctions qui prennent un paramètre implicite qui est de type produit.

Par exemple, un type que l'on peut convertir en chaîne de caractères, on pourrait l'écrire comme cela en OCaml :

type 'a showable = {show : 'a -> string}

(* puis l'utiliser ainsi *)
let print dict value = print_endline (dict.show value);;
val print : 'a showable -> 'a -> unit = <fun>

Ce que font les interfaces de Go, les types classes ou les traits c'est instancier implicitement le dictionnaire de méthodes en fonction du type du paramètre value. De telle sorte qu'il suffit d'écrire print 1 au lieu de print {show = string_of_int} 1. Mais un dictionnaire, cela reste un type produit. C'est surtout utilisé pour faire du polymorphisme ad hoc, et non pour se substituer au type somme.

Pour faire la même chose en OCaml, avec la même généralité que les type classes de Haskell, il faudrait passer par le système des modules et foncteurs. Un module est un dictionnaire (type produit), qu'il faudrait passer comme argument implicite à une fonction. Il faut pour cela étendre le système des modules de première classes (en faire des valeurs comme les autres), puis ajouter un système de résolution pour arguments implicites. C'est un objet de recherche en cours.

J'ai pas vu passer ça ! J'imagine que c'est une extension ppx, ou alors directement intégré dans le langage ?

C'est du sucre syntaxique intégré au langage depuis la version 4.08, mais c'est inspiré de ce qui se faisait avant avec des extensions ppx. Cela a été fait pour simplifier le code qui utilise des monades ou des foncteurs applicatifs (cf. la doc sur les binding operators). Je trouve que cela rend mieux compte du choix du nom bind pour l'opérateur monadique que ne le fait la do notation de Haskell. Le >>= c'est juste une généralisation du pipe du shell qui est le bind de la monade identité.

Le code avec les exceptions j'aurais pu l'écrire ainsi si j'avais utilisé le pipe :

let test i j =
  int_of_string i |> fun i ->
  int_of_string j |> fun j ->
  i + j

ou avec la type classe de la monade identité :

let (>>=) = (|>)
let return x = x

let test i j =
  int_of_string i >>= fun i ->
  int_of_string j >>= fun j ->
  return (i + j)

Ce qui est le même code que la version monadique avec le type option. Réciproquement, le sucre syntaxique des binding operators permet de récupérer la forme non monadique pour du code monadique.

En Rust, ils se sont contentés de sucre syntaxique à l'aide d'une macro ? spécifique au cas du type option pour une erreur (type Result).

Comme OCaml maintenant, si je comprends bien.

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

Outre le cas de gestion des erreurs en renvoyant un type somme, il me semble étrange qu'un langage moderne ne dispose pas de types sommes. Cela ne rend pas le système de type plus complexe, ni plus dur à implémenter.

Les adeptes des types algébriques ont un slogan qui dit « types as propositions », qui est à mon sens un abus de langage. Un type c'est un concept, mais un concept il faut d'abord le définir et pour cela utiliser une… proposition. Le slogan confond, d'une certaine façon, le défini avec sa définition. Mais, ceci étant, l'absence de type somme fait que l'on ne peut pas écrire de définition disjonctive (type somme) mais seulement des définitions conjonctives (type produit, comme les couples). La disjonction (ou somme) c'est le dual de la conjonction (ou produit) : son absence est difficilement justifiable. Que dirai-t-on d'un langage qui ne fournirait pas l'opérateur xor sur un type booléen mais seulement le and ? Il amputerait grandement les capacités d'expression du programmeur.

En revanche, il est vrai que la gestion d'un tel type somme pour la gestion des erreurs peut rendre le code plus verbeux sans constructions adéquates dans le langage. Cela oblige à travailler dans une monade et, jusqu'à l'an dernier, c'était assez lourd syntaxiquement en OCaml. Contrairement à Haskell et sa do notation, mais je ne sais pas comment s'y prend Rust.

D'ailleurs, pour reprendre une partie de ton journal, c'était moins lourd de travailler avec des exceptions que des type option ou result.

let test i j =
  let i = int_of_string i in
  let j = int_of_strinf j in
  i + j

test "12" "5";;
- : int = 17

test "coin" "5";;
Exception: Failure "int_of_string".

Si on prend une fonction de conversion qui renvoie une option au lieu d'une exception cela devient beaucoup plus lourd :

let ios s = try Some (int_of_string s) with _ -> None

let test i j =
  match ios i with
  | None -> None
  | Some i -> match ios j with
     | None -> None
     | Some j -> Some (i + j)

test "12" "5";;
- : int option = Some 17

test "coin" "5";;
- : int option = None

Ou alors, pour être plus générique dans le pattern de code, on utilisera la monade d'option (ce qui complique grandement la charge cognitive pour le programmeur).

let (>>=) o f = match o with None -> None | Some x -> f x
let return x = Some x

let test i j =
  ios i >>= fun i ->
  ios j >>= fun j ->
  return (i + j)

test "12" "5";;
- : int option = Some 17

test "coin" "5";;
- : int option = None

Heureusement, depuis un an, on peut écrire un code moins abscons et plus proche de la version avec exception, mais c'est très récent.

let (let*) = (>>=)

let test i j =
  let* i = ios i in
  let* j = ios j in
  return (i + j)

test "12" "5";;
- : int option = Some 17

test "coin" "5";;
- : int option = None

N'ayant jamais utiliser Rust, on doit s'y prendre comment pour travailler dans une telle monade ?

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

Oui, on peut dire pleins de choses sur la non élégance de cet algo, mais c'est vraiment un truc comme ça que j'ai appris.

C'est le bon algo, avec néanmoins une comparaison inutile entre les deux nombres. Le principe est celui-ci :

1. prendre deux nombres a et b
2. calculer le reste r de la division de a par b
3. si r est nul, b est le pgcd recherché
4. sinon recommencer en 1 avec b et r

et c'est ce que fait ma boucle en un one liner. Il n'est pas nécessaire de chercher à savoir lequel des deux nombres est le plus grand. Si b est plus grand que a, le reste est a, et le point 4 remet tout dans le bon ordre au premier tour. Ensuite, le reste, qui servira de diviseur, sera toujours plus petit que le dividende.

De ce que je lis 40% des élèves n'y arrivaient pas.

J'ai eu beau cherché dans ce document, je ne vois pas d'où tu tires ce nombre. De mémoire, on était bien moins de 60% à y arriver. J'ai raconté cette anecdote pour montrer que le changement de base était accessible à certain élèves de primaires (les plus doués en maths d'entre eux) et qu'il devait donc être une formalité pour des étudiants dans le supérieur (ceux qui font des études d'info). Ceci étant, je me demande la part d'enfants qui appliquent sans comprendre et ceux qui comprennent réellement : la raison leur est enseignée (voir par exemple la chaîne lumni lancée pendant le confinement) mais combien la retienne et la comprenne réellement, je ne le sais.

Ceci étant, je maintiens que, comme pour le pgcg, l'alogrithme est hautement récursif et fonctionnel :

let ajouter_chiffre c1 c2 =
  let res = c1 + c2 in
  if res < 10 then (res, 0) else (res - 10 , 1)

let additionner l1 l2 =
  let rec loop (res, retenue) m n =
    match m, n with
    | c1 :: reste1, c2 :: reste2 ->
       let c, retenue = ajouter_chiffre c1 (c2 + retenue) in
       loop (c ::res, retenue) reste1 reste2
    | [], c :: reste | c :: reste, [] ->
       let c, retenue = ajouter_chiffre c (0 + retenue) in
       loop (c :: res, retenue) [] reste
    | [], [] ->
       List.rev (if retenue = 0 then res else retenue :: res)
  in loop ([], 0) l1 l2

(* 1 + 999 = 1000 *)
additionner [1] [9; 9; 9];;
- : int list = [0; 0; 0; 1]

(* 31 + 35 = 66 *)
additionner [1; 3] [5; 3];;
- : int list = [6; 6]

Ici les nombres sont représentés par une liste de chifres en mode "petit boutiste". Le code lui même reproduit parfaitement les différentes étapes d'apprentissage d'un enfant, et les sources d'erreurs potentielles où il faut prendre garde.

L'on apprend d'abord à ajouter des chiffres de petites tailles. Ma nièce en CP est à ce stade là, elle n'a pas encore à gérer le cas de la retenue dans la fonction ajouter_chiffre. Ensuite, lorsque la somme dépasse la dizaine, on leur enseigne que l'on crée un paquet de dix (ou dizaine) et que l'on garde le reste : deuxième branche du if then else de la fonction ajouter_chiffre. C'est là que se situe l'origine et la raison d'être de la retenue.

Ensuite, lorsque l'on pose l'addition, on a deux listes de chiffres puis l'on a va en construire une autre (sans modifier les deux en entrées) en appliquant itérativement (c'est-à-dire récursivement) l'addition de chiffre sur nos deux listes jusqu'à épuisement complet.

De plus, les différentes branches montre bien deux sources d'erreurs ou de confusion qui arrive au cours de l'apprentissage :

• la première étant qu'un enfant peut ne pas savoir quoi faire lorsqu'il a épuisé une liste mais pas l'autre (deuxième branche du code)
• la seconde étant qu'au début ils leur arrivent souvent d'oublier de redescendre la retenue s'il en reste une à la fin (le if then else de la dernière branche).

Enfin, la méthode est facilement généralisable pour un programmeur (ou un enfant dont le niveau d'abstraction est suffisamment développé). Ici la base est codée en dur dans l'addition de chiffres : il suffit d'en faire un paramètre. ;-)

(* le tilde ~ devant le paramètre est là pour avoir
    un paramètre nommé *)
let ajoute_chiffre ~base c1 c2 =
  let res = c1 + c2 in
  if res < base then (res, 0) else (res - base , 1)

let additionner ~base l1 l2 =
  let rec loop (res, retenue) m n =
    match m, n with
    | c1 :: reste1, c2 :: reste2 ->
       let c, retenue = ajoute_chiffre ~base c1 (c2 + retenue) in
       loop (c ::res, retenue) reste1 reste2
    | [], c :: reste | c :: reste, [] ->
       let c, retenue = ajoute_chiffre c ~base (0 + retenue) in
       loop (c :: res, retenue) [] reste
    | [], [] ->
       List.rev (if retenue = 0 then res else retenue :: res)
  in loop ([], 0) l1 l2

(* exemples *)
(* 31 + 35 = 66 en base 10 *)
additionner ~base:10 [1; 3] [5; 3];;
- : int list = [6; 6]

(* la même en base 16 *)
additionner ~base:16 [15; 1] [3; 2];;
- : int list = [2; 4]

(* puis en base 13 *)
additionner ~base:13 [5; 2] [9; 2];;
- : int list = [1; 5]

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

Je ne vais reprendre qu'une partie car il me semble que c'est le nœud de notre désaccord.

Il y a bien là un point de désaccord, tu sembles, à mes yeux, sous estimer grandement les capacités intellectuelles et de compréhension d'un enfant.

Je vais d'abord parler d'un personne que je connais bien : moi-même. J'ai effectué mon école primaire dans les années 80 au sein d'une école privée. Pour l'accès au collège, il y avait un examen d'entrée en 6ème. Parmi les exercices de calculs, il y en avait un qui consistait à effectuer une addition et une multiplication en base 10… puis en base 5. Il fallait ensuite convertir les résultats d'une base à l'autre pour bien vérifier que le résultat était indépendant de la base choisie.

Oui : on demandait cela à des élèves en fin de CM2. Je t'accorde que tous n'y arrivaient pas, mais j'étais loin d'être le seul à y arriver, et nous comprenions ce que nous faisions. On ne se contentait pas d'appliquer bêtement une recette sans savoir pourquoi elle fonctionne. Je suppose que le choix des bases était fait à partir du nombre de doigts que l'on possède sur nos mains. Mais dans le fond, pas de grande différence, sur le plan algorithmique, avec une base 2, 8 ou 16.

Ensuite, pour les enfants d'aujourd'hui, je n'ai comme exemple proche que mes nièces, n'ayant pas d'enfants. Elles sont en 5ème, CM1 et CP. Les deux grandes comprennent leurs algorithmes, à commencer par la raison d'être de la retenue, quand à la dernière je lui ai déjà appris les petites additions à deux chiffres sans retenue. Et non, elles n'appliquent pas bêtement une recette sans la comprendre.

surtout que ton exemple est généralement présenté comme itératif et non fonctionnel

Euh, une récursion fonctionnelle c'est itératif. Elle est où ta distinction ? Un procédé récursif ou itératif, c'est bonnet blanc et blanc bonnet. Quand une personne se dit que pour une poule, il faut un œuf, mais que pour un œuf, il faut aussi une poule, puis qu'elle réitère (note bien le choix du verbe), elle fait de la récursion. Le problème ici étant : quelle est la condition d'arrêt ?

Mais rassure moi, pour l'algorithme d'Euclide, on ne vous le présentait pas autrement qu'avec ce one liner ?

let rec pgcd a b = match (a mod b) with 0 -> b | r -> pgcd b r

(* exemple *)
pgcd 21 15;;
- : int = 3

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