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 :
typeA|Bmatchvwith|OkA->...|OkB->...|Error_->...(* comparé à *)matchvwith|Okv->matchvwithA->...|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_int1;;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.
[^] # Re: Raisons d'essayer Rust
Posté par kantien . En réponse au journal Retour d'expérience sur les langages de programmation. Évalué à 1. Dernière modification le 19 novembre 2020 à 16:20.
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_coldans ce journal de gasche. Ou celui-ci :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.
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
topet 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 etinterface {}, ils ne se passe rien, tout va bien :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").
Les extensions de syntaxes ppx dérivent un pretty printer (
pp) à utiliser comme celui fournit par défaut pour lesint. 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.