kantien a écrit 1187 commentaires

La gestion des permissions, quand à elle, reste correcte d'un point de vue système

Même là c'est douteux. Si les services de l'État viennent détruire ta maison, sous ce très pernicieux prétexte, que j'en ai mis l'ordre de mission sur leur bureau, je doute que tu considères que la gestion des permissions reste correcte d'un point de vue système. ;-)

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

Ce langage est trop matheux à mon goût.

C'est une question de goût : personnellement, c'est pour cela que je l'aime. Un ordinateur, ça sert à calculer et tout ce qui s'éloigne, de près ou de loin, de la pratique mathématique en la matière, finit irrémédiablement à la poubelle chez moi. De plus, les mathématiciens, outre leur quête de rigueur, ont un penchant naturel pour une recherche d'esthétisme dans leur notation et la structure de leur discours : esthétisme que je ne retrouve pas dans les autres langages.

Les mathématiques ont un triple but. Elles doivent fournir un instrument pour l’étude de la nature.

Mais ce n’est pas tout : elles ont un but philosophique et, j’ose le dire, un but esthétique. Elles doivent aider le philosophe à approfondir les notions de nombre, d’espace, de temps.

Et surtout leurs adeptes y trouvent des jouissances analogues à celles que donnent la peinture et la musique. Ils admirent la délicate harmonie des nombres et des formes ; ils s’émerveillent quand une découverte nouvelle leur ouvre une perspective inattendue ; et la joie qu’ils éprouvent ainsi n’a-t-elle pas le caractère esthétique, bien que les sens n’y prennent aucune part ? Peu de privilégiés sont appelés à la goûter pleinement, cela est vrai, mais n’est-ce pas ce qui arrive pour les arts les plus nobles ?

Henri Poincaré, la valeur de la science

Tu dois avoir des problèmes de souvenir sur ce que te disait ton prof.

Ton explication par exemple de :
val compare : t -> (t -> int)

Je me rappelle de mon prof qui disait qu'on pouvait le lire aussi:
val compare : (t -> t) -> int

Donc ça prend une fonction de t vers t et ça renvoie un int (qui de mon point de vue se rapproche davantage du "je prends 2 arguments et je renvoie un entier vrai/faux".

Je ne vois pas comment tu peux lire la seconde signature comme "je prends 2 arguments", alors qu'elle n'en prend qu'un qui est une fonction. De plus, on ne peut pas lire la première comme la seconde, mais celle-là est équivalente à une fonction avec cette signature :

val compare : t * t -> int

qui se lit déjà mieux comme "je prends 2 arguments…". Mais quand je dis qu'elles sont équivalentes, je ne veux pas dire que ce sont les mêmes, mais que je peux passer de l'une à l'autre et qu'elles calculeront la même chose. Le passage de l'une à l'autre se nomme curryfication mais ce n'est absolument pas propre à OCaml, comme l'illustre l'article de wikipédia. Ce passage de l'un à l'autre, ou cette équivalence, est identique à cette identité algébrique sur l'exponentielle et le produit :

(A ^ B) ^ C = A ^ (B * C)

L'exponentielle c'est le type des fonctions (la flèche -> lue de droite à gauche) et le produit c'est le produit cartésien sur les types (pour créer des paires).

La version à la Curry permet de définir simplement des clôtures ou des applications partielles, comme dans cet exemple :

List.map (compare 2) [1; 2; 3; 4; 5]

D'ailleurs, au sens propre du terme, une fonction n'a toujours qu'un seul argument. Dans la version non curryfiée, il se trouve que cet unique argument est une paire (d'où la lecture "je prends 2 arguments…"), ce qu'il n'est pas dans la version à la Curry.

En ce qui concerne, l'intérêt des fonctions qui retournent des fonctions (t -> (t -> int)) et des clôtures, tu pourras lire la discussion que l'on a eu récemment sur les génériques dans Go. Ici @wilk donne un lien vers un article qui, pour présenter la notion de clôture en Go, définit justement une fonction qui retourne une fonction.

Je ne pourrai jamais m'intéresser à un projet codé en (O)Caml, aussi intéressant puisse-t-il être.

Je n'aime pas l'ananas mais je crois, qu'ici, tout le monde s'en fout, et je ne vois pas bien l'intérêt d'exprimer la chose publiquement. Dans le cas présent, je doute que les auteurs du projet puissent être, pour leur part, intéresser pas les contributions que tu pourrais apporter.

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

Bon, quand on regarde en détail, je préfère

int compare(a: T, b : T);

(les fonctions façon LISP… pour compare et add dans cet exemple) à

val compare : t -> t -> int

C'est une question de point de vue, et je trouve la syntaxe OCaml bien plus cohérente quand on la regarde dans l'ensemble du langage.

Une expression de la forme val e : t se lit « e est une valeur de type t », et je ne vois pas pourquoi il faudrait changer de forme, sous prétexte que la valeur compare est ici une fonction. Le : de OCaml c'est comme le epsilon () des mathématiciens, il signifie l'appartenance à un ensemble. Ici, c'est l'ensemble des fonctions des t vers les fonctions des t dans les int (ça se lit t -> (t -> int)), c'est une fonction qui renvoie une fonction. De même, la fonction successeur sur les entiers a pour type int -> int, c'est une fonction des int vers les int.

En résumé, on a donc un nom pour la valeur, suivi du : (le epsilon des matheux, ou le est du français comme dans « Socrate est un homme ») puis enfin une expression qui appartient au langage des types.

Cette dernière expression, on pourrait la réutiliser telle quelle dans le langage des types, pour définir par exemple un type paramétrique, comme ici :

type 'a comparator = 'a -> 'a -> int

Ici comparator est une fonction des types dans les types (un type paramétrique) et 'a est le nom de son paramètre. On peut alors réécrire la signature du début ainsi:

(* la fonction `comparator` appliquée au type `t` *)
val compare : t comparator (* t -> t -> int *)

Il y a en fait 4 langages dans OCaml :

• le langage des valeurs et expressions
• le langage des types des expressions
• le langage des modules
• le langage des types de modules ou signatures

Les deux derniers, dont tu préfères la syntaxe, ont « globalement » les même principe syntaxiques que les deux premiers qui semblent te désarçonner. Pourquoi ?

Pour le foncteur Make, on aurait pu écrire sa signature ainsi :

module Make : functor (S : ORDERED) -> sig ... end

ce qui est la même syntaxe que pour compare, à part le mot clef functor (personnellement, je le trouve inutile et j'aurais préféré qu'il soit absent, je trouve qu'il alourdit sans raison l'écriture et la lecture).

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

Je ne vois pas de fermeture dans l'exemple que tu donnes par contre ?

Les fonctions Abs sont des fermetures, une interface c'est un dictionnaire de fermetures. Prenons le code d'usage de l'interface :

func main() {
    var a Abser
    f := MyFloat(-math.Sqrt2)
    v := Vertex{3, 4}

    a = f  // a MyFloat implements Abser
    a = &v // a *Vertex implements Abser

    // In the following line, v is a Vertex (not *Vertex)
    // and does NOT implement Abser.
    a = v

    fmt.Println(a.Abs())
}

la variable a est un dictionnaire de fermeture et a.Abs est une fermeture (la variable capturée étant soit un Myfloat, soit un *Vertex). Il en est de même pour n'importe quelle interface. C'est pareil en POO : un objet c'est un dictionnaire de fermetures qui partagent le même environnement (les variables d'instance). C'est un usage classique des fermetures pour faire du polymoprhisme ad-hoc, qui est celui que tu décris, avec de l'encapsulation. Cela permet d'utiliser, comme expliqué dans l'article que tu cites sur medium, le même algorithme sur différentes structures de données qui partagent un comportement commun (décrit par l'interface).

Voyons voir ce qu'est une fermeture (je l'écris en OCaml, c'est plus simple pour moi, surtout pour la suite).

let foo i j = 2 * i + j

ici la fonction foo est dite close car toutes les variables qui apparaissent dans son code sont des paramètres formels de celle-ci. En revanche ce n'est plus le cas celle-ci:

let i = 2
let bar j = 2 * i + j

ici la variable i fait partie de l'environnement de bar (on dit que i apparaît libre dans bar, là où il est lié dans foo), cette dernière est une application partielle de foo: let bar = foo 2. La fermeture consiste à transformer bar en une paire constituée de la fonction close foo et du paramètre i = 2 : une fonction non close est transformée en une fonction close, on la clôture ;-)

Reprenons maintenant l'interface Abser de l'exemple en go:

type Abser interface {
    Abs() float64
}

En OCaml, on écrirait cela ainsi :

type abser = { abs : unit -> float }

mais ce type sera habité par des fermetures, c'est à dire des paires dont la fonction close aura cette forme :

type 'a abser_close = { abs : 'a -> float }

et la clôture aura cette forme :

type 'a abser_closure = 'a abser_close * 'a

autrement dit une fonction sans variable libre sur une type 'a, ainsi qu'une valeur de ce même type 'a correspondant à celle qui est capturée et encapsulée dans la clôture. Maintenant le type de départ abser est équivalent à la réunion (ou somme) sur tous les types possibles des fermetures précédentes :

type abser = Abser : 'a abser_closure -> abser

Géométriquement, on peut représenter cela par un cône:

La base circulaire représente tous les types possibles du langage et le sommet est justement le type abser. Ce cône peut être vu comme un graphe orienté étiqueté, où chaque arrête va de la base vers le sommet avec comme étiquette la fonction qui calcule la valeur absolue pour le type en question. Il illustre comment on transforme un Myfloat ou un *Vertex en un Abser. Maintenant, quand on veut utiliser un Abser, il faut retourner l'orientation du graphe : on ne va plus de la base vers le sommet, mais du sommet vers la base. Alors une valeur de type Abser ne peut être utilisée quand observant la valeur qu'elle encapsule, en redescendant le long de l'arrête correspondant et en appliquant la fonction en étiquette. Ce mécanisme d'utilisation d'un Abser est ce que les programmeurs appellent le dynamic dispatch, qui est au cœur de la POO et du polymorphisme ad-hoc.

La généricité, en revanche, permet d'appliquer le même algorithme sur un même structure de données qui est un conteneur, comme le sont les tableaux (on parle plutôt volontiers, dans ce cas, de polymorphisme structurel). Ici, vous vous en sortez avec des fermetures (comme pour la fonction de tri), parce qu'un tableau peut être vu comme un dictionnaire clef-valeur où les clefs sont des int. Ainsi, au lieu d'avoir une fonction avec un type polymorphe, qui prend une fonction de comparaison sur le type contenu dans le tableau ('a -> 'a > bool), vous pouvez vous contentez d'un type monomoprhe int -> int -> bool en encapsulant le tableau et en accédant aux valeurs par leur index. Mais cela réduit la généricité au tableaux, qui sont built-in, et cela ne permet pas de créer ses propres type génériques.

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

Je ne sais pas.

Moi non plus. Ce qui me fait douter du fait que wilk comprenne bien ce qu'est le système de interfaces, ainsi que le manque que vient combler le système des génériques. L'idée derrière ce système étant de pouvoir retrouver, dans le système de types, le type de la variable capturée dans l'environnement des fermetures que constitue l'interface. Alors qu'avant il pouvait seulement le retrouver par un switch sur type dans le code (d'où le nombre important de code qui prennent un interface {} en entrée). Il pouvait réfléchir dans le code, mais non dans le système de types, la structure de l'environnement de leurs fermetures.

Si on prend l'exemple de a tour of go:

type MyFloat float64

func (f MyFloat) Abs() float64 {
    if f < 0 {
        return float64(-f)
    }
    return float64(f)
}

type Vertex struct {
    X, Y float64
}

func (v *Vertex) Abs() float64 {
    return math.Sqrt(v.X*v.X + v.Y*v.Y)
}

On voit bien, sur leur déclaration, que les deux méthodes Abs sont des fermetures : la première capture un MyFloat et la seconde un *Vertex. Les génériques permettent juste de donner un nom de variable au type de la valeur capturée pour l'utiliser dans la signature des fonctions.

soit n'ont pas besoin de ça

Ça fait un peu « dis moi ce dont tu as besoin, je te dirais comment t'en passer ».

soit tu te crée que des méthodes et pas des fonctions. Tu modifie les paramètres que l'on te donne plutôt que de retourner quelque chose.

Même le tri en place du tableau, je doute que ce soit possible (génériquement) en golang avec seulement des interfaces (pour la bonne raison qu'une fonction d'ordre est un opérateur binaire, ce qui n'est pas gérer par les interfaces de base).

Après, qu'il existe des contournements, en l'absence de généricité, pour résoudre les problèmes que l'on a, je n'en doute pas. Là où je suis plus sceptique, c'est qu'ils auront plutôt tendance à compliquer le code et non le simplifier.

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

Le code n'a plus de lien avec le type de l'objet capturé avec la fermeture, mais avec le comportement de la fermeture elle même.

J'aurais du préciser : sans perdre le lien entre le type d'entrée et le type de sortie. ;-)

Sinon ce que tu décris c'est tout simplement le fonctionnement des interfaces jusqu'alors : une interface c'est juste un dictionnaire de fermetures. D'ailleurs pourquoi passer par des fermetures à sa sauce quand le langage fournit nativement un tel mécanisme ?

Un cas d'exemple simple et générique impossible à rendre, au niveau des types, avec les interfaces (ou fermetures) : le tri d'un tableau. Quand on a un tableau sur un type ordonné (que le type soit ordonné cela s'exprime par le fait qu'il satisfait une certaine interface), alors on peut trier (par ordre croissant ou décroissant) ce tableau : le type de sortie dépend du type de l'entrée, en sortie on a un tableau sur le même type de données qu'en entrée.

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

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.