anaseto a écrit 2229 commentaires

Ça vient autant des gens voulant faire croire qu'il y a une différence entre open source et libre

Le sens des mots varie suivant les communautés et les sensibilités personnelles, c'est naturel et scientifique (au sens linguistique). Personnellement, mon impression est que l'open source et le libre utilisent le même type de licence, mais pour des raisons différentes et qu'il y en a comme toi qui veulent nier l'existence de cet aspect plus idéologique des choses, je sais pas trop pourquoi, d'ailleurs. C'est inévitable que parfois des mots proches développent des nuances différentes, ce genre de choses se produit spontanément et en permanence.

Bien pessimiste ton drame :-)

C'est sûr qu'en fonction des besoins et la chance, ça peut être plus ou moins compliqué. Ceci dit, perso, ça fait plein d'années que j'autohéberge mes mails et un site web statique sur OpenBSD sur une vieille machine (32 bits, 2Go de ram) sans rien changer (à part lancer un syspatch de temps en temps et maintenant un sysupgrade tous les six mois). Et mes mails semblent d'ailleurs encore arriver à mes correspondants, au point que j'en suis même surpris, car je fais même pas les choses bien : j'ai pas fait l'effort de mettre du DKIM et ça fait un moment déjà que c'est à la mode.

Je suis près à remplacer systemd par autre chose qui serait objectivement meilleur, mais en attendant Debian a énormément gagné en sérieux en intégrant systemd.

Comme tu le dis, ça dépend beaucoup de la distribution. Et ça dépend aussi beaucoup de ce qu'on fait avec. Personnellement, sous OpenBSD, j'ai jamais touché quoi que ce soit à l'init : j'ai même pas besoin de savoir que c'est des scripts. Du coup, forcément, changer ça par quelque chose comme systemd, qui représente un programme d'un voire deux ordres de grandeurs de plus en taille, n'aurait pas de sens pour moi, juste une source potentielle de nouveaux bugs de sécurité ou de mauvaise intégration (sous OpenBSD rc + rc.sub c'est moins de 1000 lignes de code, et en ajoutant tous les scripts chez moi ça arrive tout juste à 1500, ça reste dans le domaine du maintenable pour du shell).

Tiens, je connaissais pas cette histoire (ou j'ai oublié). Ceci dit (haha), le wiktionnaire, assez descriptif plutôt que prescriptif dans son approche, documente l'expression, en mentionnant bien cependant que certains « puristes » y trouvent effectivement quelque chose à redire :-)

Personnellement, d'un point de vue linguistique, j'ai l'impression que « cela » est en voie de disparition de la langue (orale), remplacé par « ça » la plupart du temps, ou « ceci » dans certaines expressions (« ça dit », qui serait la contraction théoriquement « correcte » ne s'utilise pas, il me semble).

Après tout, il se peut que je me sois emporté parce que c'est un sujet (sur le plan scientifique1, 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.

J'ai répondu un peu plus bas à des choses proches, mais vraiment, la source de notre différence de perspective est que tu ne considères que l'aspect théorie logique/théorie des types dans tes réponses, alors que nous autres nous intéressons plutôt aux interactions de l'humain avec le système de types et le langage en général.

La question de savoir si l'utilisation des interfaces à la place d'un type somme est équivalente d'un point de vue logique, ou la question d'utiliser un produit pour la gestion d'erreurs plutôt qu'un type somme qui semblerait plus naturel à un théoricien du typage, sont des questions dont les réponses ne fournissent pas d'impact pratique clair. Un choix optimal d'un point de vue langage n'a a priori aucune raison de devoir être compatible avec un raisonnement de logique, puisqu'il s'agit d'une science avant tout humaine : un langage de programmation est une interface entre l'humain et la machine.

Chercher à appliquer des idées de théorie des types est intéressant, mais sans statistiques comparative ni même une intuition des conséquences sur le nombre de bugs ou la productivité dans des contextes réels d'une idée ou l'autre, ce n'est vraiment pas quelque chose qu'on peut espérer pouvoir faire sans faire de concessions aux considérations humaines.

Je t'ai bien donné des réponses diverses à la question d'origine (accessibilité, simplicité du flot de contrôle et annotation facile des erreurs sans introduire de nouvelles syntaxes, analyses statiques qui évitent les soucis en pratique, etc.) pour ces choix et tu résumes le tout à « une réponse qui n'en est pas une » juste parce qu'il s'agit de réponses qui n'ont rien à voir avec la science de la logique.

À 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 somme1, 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 crois que ce que tu ne vois pas depuis le début, c'est qu'un langage de programmation est normalement utilisé par des humains pour développer des logiciels. Sa création doit donc être basée non sur une science prescriptive comme la logique, mais sur une science sociale et expérimentale et encore plus vieille, basée sur l'observation des besoins des gens et, en particulier ici, des développeurs. Un système de types puissant n'est pas forcément un système de types qui conduit en pratique à une meilleure productivité ni à moins de bugs. Enfiler une armure de plates avant d'aller couper des oignons pour le repas est contre-productif et n'apporte aucune sécurité supplémentaire à moins de décider d'utiliser une épée plutôt qu'un simple couteau bon marché.

De ce point de vue là, je trouve personnellement que le système de types de Go a fait un meilleur travail que celui d'OCaml. Si j'étais rapide dans mes conclusions comme toi, je pourrais donc dire que les responsables OCaml ne maîtrisaient pas les notions de cette science sociale et expérimentale. Étant plus prudent, je pense plutôt qu'ils avaient des objectifs primaires différents avec ce langage (jouer avec les types et se faire plaisir) et que les besoins des développeurs étaient, à l'époque, beaucoup moins bien connus qu'aujourd'hui.

Perso, ce que j'ai jamais compris, c'est pourquoi ils ne font pas, comme sur OpenBSD, la différence entre les blobs au sens microcode qui est chargé sur un composant hardware particulier, et les drivers non libres (les seuls que les gens appellent blobs dans le monde BSD). Les seconds s'exécutent dans le noyau et sont vraiment problématiques pour plein de raisons, mais les premiers s'exécutent dans du matériel spécifique et n'apportent pas vraiment de problèmes qui n'existent pas déjà : que le microcode soit reçu après le démarrage ou déjà présent dans le matériel, ça ne change pas grand chose au final, à moins d'avoir du matériel libre à la base.

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.

Pour te rassurer, c'est comme cela que je l'ai pris, mais ce n'est pas comme cela que tu l'as écrit, il y avait un point après « sérieux » : facile à interpréter plus génériquement :-)

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 ?

Oui, mais l'histoire de la réflexion est sortie suite à une question initiale sur les applications intéressantes (au sens général a priori) de celles-ci : à aucun moment je n'ai essayé de te convaincre que ça serait intéressant pour toi en particulier, mais de t'informer à ta demande pourquoi ça l'était pour d'autres. C'est pour ça qu'on se répète, parce que j'ai répondu à cela et tu n'as, par la suite, qu'uniquement insisté sur le fait que tu n'en avais rien à faire et que c'était question de goût, ce qui était HS et donne l'impression que tu te fiches de l'intérêt de la chose en général, même si ce n'est pas ton intention.

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.

Encore une fois, c'est effectivement ce que j'ai imaginé de ta part. Mais ce n'est pas évident dans tes messages. 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 : c'est l'interprétation la plus naturelle pour un programmeur, c'est-à-dire les premiers utilisateurs de langages de programmation qui n'imaginent pas forcément que pour d'autres, un langage de programmation, c'est un terrain d'expérimentation pour jouer avec les types. Pour le coup, ils risquent de ne pas trouver ça sérieux, tu es en train de jouer après tout, même si c'est avec un système de types sérieux ;-)

Ce n'est donc pas ton insistance à affirmer que Go a des types somme qui m'arrêtera.

Si tu relis mes messages, tu verras que depuis le début je n'ai pas vraiment affirmé cela (le débat de théorie des typages n'est pas inintéressant pour moi, mais secondaire). Plutôt, j'ai affirmé que je pouvais traiter (ou encoder) avec des types Go les cas d'utilisation (pratique de programmation) des types sommes. Je n'affirme même pas que mon énoncé a un sens propre en théorie des types. Et j'ai fait l'effort de donner des exemples à l'appui pour chaque chose que tu as demandé (en commençant par les listes chaînées), avec l'idée que tu t'intéressais au langage et pas uniquement à faire rentrer son système de types dans ton jeu sur les systèmes de types. Quand j'ai dit utilisation ou pratique de programmation, c'est dans un sens pratique, pas au sens d'un énoncé de typage précis : les cas d'utilisation que j'ai pu rencontrer personnellement, que ce soit dans CompCert en Coq ou dans OCaml (ce que j'ai précisé ensuite). J'ai bien reconnu d'emblée que ce soit plus verbeux, ou l'absence de gestion de la distinction ouverte ou fermée : distinction peut-être capitale pour qui utilise le langage comme plateforme de jeu sur les types, mais distinction beaucoup plus secondaire autrement.

Pour en revenir sur les goûts : si tu relis mes messages sur ce fil, tu verras que je ne parle pas vraiment de mes goûts (je l'ai déjà fait dans le journal), mais de pourquoi, à mon avis, les choses sont ainsi en Go. Concernant mes goûts, vu le journal, c'est assez clair qu'ils sont variés et, suivant ce que je veux faire (jouer avec les types, les tableaux multi-dimensionnels ou développer un logiciel) j'utilise quelque chose de différent. Le système de types de Go n'est pour moi ni meilleur ni pire dans l'absolu que celui d'OCaml : il répond simplement à des besoins et un public différents. Je n'affirme pas par là que leur champ d'application est sans intersection en pratique (ce n'est pas le cas), mais que, globalement, Go est plus un langage dont le design vise à répondre aux besoins des développeurs, alors qu'OCaml vise avant tout à répondre aux besoins des chercheurs en théorie des types.

A priori les fonctions génériques seront compilées une seule fois :

Generic functions, rather than generic types, can probably be compiled using an interface-based approach. That will optimize compile time, in that the function is only compiled once, but there will be some run time cost.

J'imagine que définir les contraintes pour les types génériques à l'aide d'interfaces rend cette approche assez naturelle. Rien dans le draft n'impose vraiment une approche ou l'autre, ceci dit.

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).

Parce c'est plus simple pour le flot de contrôle et se gère plus naturellement et légèrement avec les structures de contrôle impératives classiques déjà présentes. Go n'est pas un langage où les gens veulent une étude continue de nouvelles fonctionnalités syntaxiques.

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.

La notion de système de types sérieux ou non n'est pas constructive : perso, je comprends que c'est une façon de transmettre ton ressenti et, connaissant bien OCaml, je peux prendre ça avec recul. 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.

Le but d'un langage de programmation, ce n'est pas son système de typage, c'est d'écrire des programmes qui répondent à des besoins. Et concernant le typage, tout n'est pas question de puissance, mais aussi d'accessibilité en pratique : c'est pas pour rien que les modules en OCaml sont sous-utilisés et considérés un concept pour non-débutants par rapport aux interfaces Go, accessibles aux débutants, par exemple. Le but des types somme pour les errerus, c'est de bien gérer ces erreurs : d'autres approches comme celle de Go permettent statistiquement de bien gérer les erreurs aussi (voire mieux que les exceptions OCaml), sont-elles moins sérieuses ? La réflection permet grâce au marshalling de sauver facilement un état (par exemple sauvegarde pour un jeu) sans avoir à écrire de code, c'est une application pratique, peu importe le sérieux de l'approche par rapport à une autre approche qui ne propose pas encore d'équivalent simple.

C'est beaucoup moins puissant, mais aussi beaucoup moins compliqué (tant pour l'utilisateur que l'implémentation). Mais faut dire que les modules paramétriques OCaml sont vraiment puissants par rapport à ce qu'on trouve ailleurs.

Dans les différences concrètes que je peux voir se produire en pratique, il n'est par exemple pas possible d'utiliser une fonction générique autrement que pour l'instantier ou l'appeler (donc, si j'ai bien compris le draft, tu ne pourras pas faire une fonction qui renvoie une fonction générique, par exemple). On peut aussi uniquement paramétrer par des types et non des valeurs. Pas de généricité dans les paramètres de méthode non plus (la question de savoir si une méthode permet de satisfaire une interface deviendrait floue).

J'aimais pas trop certains drafts précédents, mais le dernier je le trouve pas mal : faudra voir ce que ça donne et couvre statistiquement en pratique.

J'ai lu le fil de discussion, et je suis honnêtement un peu dans la même situation que schonfeder à la fin

J'ai lu un peu les pages suivantes : l'exemple de trefis est intéressant et montre une différence plus significative (un seul raise au lieu de trois), au prix d'une formule un peu longue.

Ceci dit la version proposée utilisant les types somme actuels :

match f () with
| Some y ->
  begin match g y with
  | A x ->
    begin match h x with
    | Ok result -> result
    | Error _ -> raise Not_found
    end
  | _ -> raise Not_found
  end
| None -> raise Not_found

ressemblerait beaucoup à la version Go naturelle :

y, err := f()
if err != nil {
   return err
}
switch x := g(y).(type) {
case A:
   result, err := h(x)
   if err != nil {
       return err
   }
   return result 
}
return errors.New("not found")

qui, dans ce cas particulier pourrait être raccourcie (mais c'est pas idiomatique) :

y, err := f()
if err == nil {
   switch x := g(y).(type) {
   case A:
      result, err := h(x)
      if err == nil {
         return result
      }
}
return errors.New("not found")

dans le même style que la solution proposée avec la nouvelle syntaxe qui fonce direct sur la seul cas intéressant :

let foo () =
  match f () with
  | Some y and (g y with A x and (h x with Ok result)) -> result
  | _ -> raise Not_found

Mais, est-ce une situation fréquente que de se retrouver avec seulement un cas qui correspond à un résultat, et tout plein de cas qui correspondent exactement à la même erreur ? Et si on veut ajouter un contexte à l'erreur au lieu d'un simple Not_found (est-ce que c'est h ou g qui n'a pas trouvé de résultat ?), la nouvelle syntaxe proposée n'est plus utilisable.

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.

J'ai lu le fil de discussion, et je suis honnêtement un peu dans la même situation que schonfeder à la fin : je suis assez perplexe quand au problème pratique que résolvent ces considérations syntaxiques, il me manque un contexte. Là, on a affaire à une discussion à propos d'une syntaxe qui n'existe que dans une extension expérimentale, sans indications du problème qu'elles rendraient significativement plus simple en pratique : c'est une réponse à cela que je cherchais avec ma question.

Peut-être suis-je biaisé dans mon expérience en OCaml et Coq. C'est surtout Compcert et lecture de quelques parties du compilateur OCaml : l'essentiel des filtrages par motif qu'on y trouve ne fait pas appel à des fonctionnalités avancées ni à des destructuration vraiment profondes, c'est du code plutôt simple, assez verbeux et accessible (peut-être la partie (f)lambda plus nouvelle fait-elle un usage plus avancé du filtrage par motif ?).

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 t'accorde cela. Note cependant que l'idée qu'il est possible pour un programmeur OCaml d'écrire du code inacessible à d'autres programmeurs OCaml ne passe pas bien dans toutes les communautés. Go est un peu une réaction en ce sens : l'idée que tout programmeur doit être capable de maîtriser le langage grosso-modo dans son ensemble, pour faciliter les contributions externes ici et là. C'est pour cela que j'ai écrit :

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

Car la possibilité de faire accepter une feature comme les GADTs dans la communauté Go est nulle, même si une de leurs applications est relativement accessible.

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). Qu'est-ce qui est plus ou moins important restera subjectif, mais il s'agit de considérations de nature différentes quand même.

La somme est ouverte et non fermée, j'ai pu y rajouter un float64 avec ce code

Oui, tout à fait.

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).

Oui.

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.

Il n'y a pas de filtrage par motif avec patterns qui vont au-delà d'un niveau de profondeur de destructuration (l'équivalent du type switch), donc il faut imbriquer des type switchs au besoin pour plus de profondeur.

Au final, c'est de mon point de vue bien une différence syntaxique, même si récursive (implémentable par macro récursive, mais macro quand même). De là à dire qu'ils perdent tout de leur intérêt et que c'est non viable, je suis un peu surpris. D'après mon expérience, les destructurations à juste un niveau de profondeur sont les plus fréquentes. La plupart des filtrages par motifs se traduisent en un seul type switch, parfois une imbrication dans certaines branches, ce qui reste dans le domaine du viable à mon avis. 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.

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.

Merci aussi, c'était intéressant d'avoir le point de vue de quelqu'un qui découvre Go avec un état d'esprit venant de OCaml. Ça m'a permis de me mettre à jour sur certaines nouveautés en OCaml !

Si je dois abandonner la sécurité du typage statique

Je n'avais pas réagit sur ça, mais ici il n'est pas question de sécurité du typage statique, mais de sémantique et d'expressivité du typage : en Go Printf est type safe, c'est sa sémantique qui est différente (affichage spécial en cas de verbe de formatage incorrect). Le cas du printf OCaml est, d'ailleurs, assez unique.

On met toujours quelque part la limite pour l'expressivité du typage : c'est un effet Pareto (20% de complexité pour 80% d'avantages), sauf qu'on ne place pas tous cette limite au même endroit (Go, OCaml ou Coq ?). La vérification absolue du format du printf, c'est sympa, mais c'est de la complexité (GADTs), pour quelque chose qui évite des erreurs pas plus fréquentes (et moins graves) qu'une erreur de signe, un accès tableau mal indexé, et bien d'autres erreurs logiques qui ne sont pas traitées en OCaml.

D'autant plus, qu'en l'occurrence c'est de la complexité pour quelque chose où une analyse statique traite la plupart des cas courants : lance go vet sur ton exemple et tu auras un warning. C'est une commande de base lancée par défaut normalement à chaque fois qu'on exécute les tests avec go test et qui lance un certain nombre d'analyses statiques.

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.

Tu compares à la version d'OCaml qui n'est pas comparable, car utilise un type format dédié et pas une chaîne de caractères (le fait que l'on écrive ça sous forme de chaîne est du sucre syntaxique). Il n'est pas possible de passer une chaîne de caractères non connue à la compilation en tant que format, par exemple. Ensuite, OCaml utilise des concepts de typage autrement plus avancés que les types sommes (les GADTs) pour réussir à faire une analyse statique de l'input de type format.

Ce n'est pas possible de faire cela en Go de façon générale, puisque Go accepte des chaînes non connues à la compilation en tant que format : il existe des analyses statiques pour chercher des erreurs dans les chaînes de format lorsque ce sont des littéraux.

Par contre, en Go, on a les verbes "%+v" et "%v" qui permettent d'afficher un type quelconque sans avoir à s'inquiéter de leur type, alors qu'en OCaml on n'a pas ça. C'est une question de compromis, difficile de tout avoir.

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

Oui, enfin, c'est un tutoriel. Notre échange ne porte pas, j'espère, sur l'application la plus commune des interfaces Go (auquel cas on serait d'accord que les types somme n'est pas cette application), mais sur leur expressivité d'un point de vue typage.

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

C'est possible d'exprimer cela à l'aide du système de types. Tu peux considérer cela tricky, si tu veux, je ne vais pas débattre sur ce genre de considérations : l'encodage demande simplement l'écriture d'une méthode vide pour affirmer que le type satisfait l'interface, donc deux fois plus verbeux qu'avec un type somme dédié.

package main

import "fmt"

type IntOrString interface {
    ImplementsIntOrString()
}

type A int
type B string

func (a A) ImplementsIntOrString() {}
func (b B) ImplementsIntOrString() {}

func main() {
    x := IntOrString(A(3))
    fmt.Printf("%+v\n", x) // affiche 3
    switch y := x.(type) { // donner le nom y à la version destructurée
    case A:
        fmt.Printf("%d\n", y) // y statiquement de type A dans cette branche
        // affiche 3
    case B:
        fmt.Printf("%s\n", y) // y statiquement de type B
    }
}

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² + A³ + A⁴ +…, j'ai un switch pour les puissances 0, 1, 2 et 3 puis un dernier pour toute puissance ≥ 4.

Là tu parles d'autre chose : tu parles de l'expressivité de la construction de filtrage par motif et de sa destructuration en profondeur qui est plus du domaine de la syntaxe (le genre de trucs qui s'implémente avec des macros en lisp ou racket). En Go, tu n'as pas de syntaxe facilitant cela. Comprenons-nous bien, c'est bien une fonctionnalité syntaxique liée aux type sommes, mais ce que tu semblais débattre c'était la fonctionnalité de typage, la possibilité même de représenter les types somme à l'aide du système de types !

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 ?

C'est une question valable : en Go tu pourrais rajouter des habitants en code utilisateur, mais ça n'affecterait que le code de l'utilisateur pour une éventuelle analyse statique d'exhaustivité, ça ne va rien casser; une façon d'éviter cela pour un utilisateur, c'est de ne pas exporter la méthode publiquement; en pratique, l'utilisateur ne va pas implémenter une méthode pour satisfaire l'interface de toutes façons.

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.

Je ne vais pas débattre de la notion de version du pauvre : perso je parle uniquement sur ce qu'il est possible ou non d'exprimer avec le système de types de façon pas trop compliquée.

Un langage à typage dynamique, comme Python, est un langage avec un seul type statique à savoir top.

Personnellement, ma définition de langage dynamique est différente (à ce titre Perl n'est pas à typage dynamique, car sans type top unique), d'où ma confusion, mais admettons. Un type top semble nécessaire pour définir un Printf avec de la réflexion (que ce soit avec du typage statique ou dynamique).

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).

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 » et de comment sont implémentées certaines choses (comme la réflection) dans d'autres langages : bien que servant pour le dispatch dynamique de méthode (typage produit), ainsi que pour la réflection, elles sont des valeurs typés statiquement et les type switchs qui permettent d'accéder au type concret sont typés 100% statiquement également. Même concernant le check d'exhaustivité, rien n'empêcherait de le faire non plus (comme le prouve l'existence d'une analyse statique dont j'ai donné le lien).

Comme tu le dis, ayant programmé dans ces quatre langages, je pense savoir ce qui est possible ou non avec un type somme et, en dehors des limites du fait de l'absence de généricité en Go, je peux représenter tout type somme comme la disjonction des types satisfaisant une interface.

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.

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. En Go, il n'y a une sorte de typage dynamique uniquement lors des assertions de type explicites, mais pour le coup c'est vraiment une question orthogonale (même si elles partagent une partie d'implémentation et concepts par simple économie d'ingénierie).

Et « le reste » c'était pour répondre à ta question annexe des applications intéressantes de la réflection et choses qu'elle peut faire et que Rust, Haskell ou OCaml ne peuvent pas faire (le préprocesseur sert uniquement à réduire la quantité de boilerplate, mais ne résout pas le problème de fond). 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.

le code compile et le compilateur émet un warning et non une erreur

Pour le coup, my bad, ça fait un moment que je fais pas d'OCaml, j'ai dû confondre avec Rust où cela produit bien une erreur et non un warning.

Petit détail : à la place de

switch LinkedList(mylist).(type) {

j'aurais du écrire :

switch l := LinkedList(mylist).(type) {

puis utiliser l et pas mylist dans le Printf (ça change rien au résultat ici, mais sinon je n'illustre pas vraiment un type switch sur une interface dont on ne connaîtrait pas le type concret).

Pas forcément, lorsque tu ajoutes un nouvel habitant au type somme, cet habitant n'est encore jamais produit par le programme. Tu fais un commit. Tu continues petit à petit à ajouter les cas traitant ce nouvel habitant avec des commits régulièrement. Quand tous les cas ont été gérés (plus de warnings), on peut enfin ajouter du code qui produit effectivement cet habitant.

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 bien pour cela que je m'étonne de leur absence.

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). Je donne un exemple plus bas pour les listes simplement chaînées.

Si j'ai bien compris, la valeur nil peut être affectée à n'importe quel type

Uniquement à un type pointeur *A (équivalent à option A), et il n'y a pas une seule valeur nil, mais une différente pour chaque type pointeur (A(nil) est différent de B(nil)). Et c'est en effet un type somme qui couvre le cas courant du type option.

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.

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).

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.

Eh bien si, mais le fichier que j'ai donné contient uniquement la définition, pour les utilisations il faut regarder ailleurs comme ici qui implémente une marche sur l'ast en faisant un switch sur le type de l'interface qui sert à représenter un nœud.

Si on peut définir un ast, on peut définir en particulier une liste simplement chaînée :

package main

import "fmt"

type LinkedList interface {
    ImplementsLinkedList()
}

type Nil struct{}

func (e Nil) ImplementsLinkedList() {}

type IntList struct {
    Head int
    Tail LinkedList
}

func (l IntList) ImplementsLinkedList() {}

func main() {
    mylist := IntList{Head: 1, Tail: IntList{Head: 2, Tail: Nil{}}}
    fmt.Printf("%+v\n", mylist)
    // affiche: {Head:1 Tail:{Head:2 Tail:{}}}
    switch LinkedList(mylist).(type) {
    case Nil:
        fmt.Printf("%+v\n", Nil{}) // n'est pas exécuté
    case IntList:
        fmt.Printf("Tête: %v, Queue: %+v\n", mylist.Head, mylist.Tail)
    }
    // affiche: Tête: 1, Queue: {Head:2 Tail:{}}
}

Ici j'ai défini un type pour les listes d'entiers : jusqu'à ce qu'on ait des types génériques en Go (dans un an ou deux), si on veut plus générique il faut utiliser interface{} à la place de int, ce qui donne des listes non limitées à un seul type, comme dans Python, Perl ou Lisp.

En pratique je sais pas si grand monde fait ceci, vu que les listes simplement chaînées n'apportent que rarement quelque chose par rapport à un tableau dynamique.

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.

Ah si, en Go c'est bien type safe : lorsque la valeur marshallée n'est plus compatible (parce que le code a évolué, par exemple, ou qu'on essaye de la récupérer dans le mauvais type), on obtient proprement une erreur.

Les types switchs sur les interfaces combinés au package reflect permettent d'inspecter les types (par exemples récupérer une liste des champs d'un struct). On peut donc définir printf récursivement sur une interface : les feuilles correspondent aux types de bases du langage (int, float64, etc.). Un exemple accessible est la définition récursive de Printf pour des types quelconques : ici on a un switch sur les types simples et un traitement différent pour les types plus complexes de type reflect.Value dans une fonction différent ici (en particulier la gestion récursives des structs, maps et tableaux).

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.

Pour Printf en Go ce que je veux dire c'est qu'il peut afficher n'importe quel type de façon générique (le type est passé sous la forme interface{} pour pouvoir l'inspecter), même ceux définis par un utilisateur : pratique pour debugger par exemple. En OCaml il faut définir un affichage pour chaque type. En Haskell et Rust c'est pareil (aux derive près qui rendent la chose un peu plus facile, mais cela reste très manuel).

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.

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. Et ce n'est pas une question d'implémentation : le langage définit explicitement ces actions pour les interfaces, donc ça fait partie du langage (beaucoup de code en dépend).

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 ?).

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). Autre exemple : printf.

À la différence qu'il faut se taper à la main ce que le compilateur Go fait automatiquement pour vous.

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 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).

Mais avec les type sommes extensibles, on perd la vérifications de l'exhaustivité lorsque l'on s'en sert. ;-)

Note que, bien que pratique, la vérification d'exhaustivité a un inconvénient : elle ne se prête pas aux modifications et réparations graduelles du code. Si tu ajoutes un habitant à ton type somme, tu casses toutes les utilisations. Inversement, si on essaie de changer les utilisations d'abord, l'exhaustivité empêche de compiler également. C'est pas forcément toujours important, mais ça se heurte à certaines façons de faire : par exemple, faire son refactoring à base de petits commits, sans casser le code entre-temps.

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.

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. L'application de méthodes permet d'en faire une utilisation en tant que type produit (instatiation implicite du dictionnaire des méthodes), mais un switch sur le type (non effacé par la compilation, contrairement aux types classes ou traits) permet d'en faire une utilisation en tant que type somme.

C'est bien une notion à cheval entre les deux, qui regroupe des applications des types somme (par exemple pour représenter un ast) et types classes/traits (utilisation type produit) sous une même notion. Elle ne va pas aussi loin sur aucun des deux aspects (type somme et produit) et est un peu plus verbeuse dans son utilisation type somme, mais elle a le mérite de traiter les deux à l'aide d'un seul concept. Enfin, en bonus, 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.

Pour le moment, on dirait qu'ils n'ont pas considéré le bénéfice (check d'exhaustivité) suffisant pour introduire un nouveau concept, même s'il n'y a pas non plus d'opposition claire.

Un truc intéressant : il existe un outil d'analyse statique qui vérifie l'exhaustivité pour des types choisis sur la base d'annotations en commentaire. J'imagine que ça peut parfois valoir le coup, même si c'est un peu verbeux.