C'est peut-être une vision tordue (pour le théoricien du typage), mais, dans les faits, c'est équivalent (au côté infini près) et simple à comprendre, même si ce n'est pas une implémentation exclusive des types somme directement calquée sur un papier de recherche.
Pas besoin d'un papier de recherche pour cela, la notion de type somme c'est du niveau licence en mathématiques : c'est la somme disjointe d'ensemble (définie par une disjonction exclusive) qui est la notion jumelle du produit cartésien (type produit défini par une conjonction). Il n'y a rien de hautement sophistiqué là-dedans. C'est bien pour cela que je m'étonne de leur absence.
D'ailleurs, outre cette représentation dynamique des types, vous avez d'autres types sommes dans le langage. Si j'ai bien compris, la valeur nil peut être affectée à n'importe quel type, ce qui fait qu'en réalité vous ne manipulez que des types options, qui est un type somme : c'est le type 1 + A pour tout type A. Ce qui fait que lorsque vous avez des fonctions qui peuvent retourner une erreur, en renvoyant une paire, vous retournez un type produit de la forme suivante : (1 + A) * (1 + B) = 1 + A + B + A*B, où l'on voit les 4 cas à gérer que déplorait Colin Pitrat dans son premier commentaire. Là où, avec un type somme de résultat, il n'y a que les deux cas A + B.
Et ce n'est pas équivalent, même dans les faits. Cela l'est tout autant que Platon définissant l'homme comme un bipède sans plumes, et Diogène le cynique de le rayer en se promenant avec un poulet déplumé tout en haranguant la foule d'un « Voici un homme ! ».
Il y a d'autres types sommes infinis que l'on ne peut définir, en tant que tel, avec Go : celui des listes par exemples. Un type somme récursif, comme celui des listes, se développe en une somme infinie : 1 + A + A^2 + A^3 + ..., c'est-à-dire la liste vide, ou les listes à un élément, ou les listes à deux éléments, ou les listes à trois éléments...
Tout ce que vous avez, c'est le type somme extensible que j'ai défini précédemment, qui est géré par le compilo et accolé dans une paire à toute valeur utilisant une interface. Puis vous faites du pattern matching dessus. Mais les seuls cas d'usage que j'ai vu, c'est avec l'interface vide pour palier le manque de polymorphisme dans le langage. L'exemple que tu m'as donné pour les arbres ne semble pas faire de d'analyse de cas sur la représentation dynamique des types, mais définir des arbres dans un langage qui n'a pas de type somme (directement définissables et accessibles au programmeur) mais que des types produits (ou struct ou enregistrements...) comme on peut le faire en C, C++, Java, Python, etc.
Ce n'est pas une petite différence ! Surtout que le « à la main » passe par le concept de GADT, qui n'est pas le plus accessible
Ce que je veux dire c'est que l'outillage est là pour avoir une représentation dynamique des types, et que ce que j'ai fait à la main le compilo pourrait le faire automatiquement. Ce n'est pas la partie la plus dure, seulement je ne crois pas que quelqu'un y ait vu un quelconque intérêt à l'implémenter.
je ne vois pas comment tu pourrais définir une fonction qui marche pour tout type (dont ceux définis ultérieurement par un utilisateur).
Je ne vois pas comment tu pourrais le faire aussi, simplement en bénéficiant d'un représentation dynamique des types. Soit la fonction est polymorphiquement paramétrique et là c'est très usuel en OCaml, soit le poylmorphisme est ad hoc et c'est le système des type classes (ou interface pour Go, mais le switch sur type ne sert à rien). Où a-t-on besoin d'une représentation dynamique des types ?
Par exemple, en Go on peut faire sans plus d'histoires un marshall et unmarshall (à l'aide du module encoding/gob) de presque n'importe quel type de façon type safe (en OCaml le module équivalent n'est pas type safe).
On peut faire de la sérialisation/déserialisation de manière type safe en OCaml, mais c'est ad hoc, il faut choisir son format. Les modules de la lib standard font cela de manière générique, ce qui ne peut être type safe. Même si l'on avait une représenation dynamique des types, je ne suis pas certain que l'on puisse réellement faire cela de manière générique et type safe.
Autre exemple : printf.
Pour faire un printf type safe il me semble qu'il faut les types dépendants, et en OCaml c'est implémenté via un GADT.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # 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 17 novembre 2020 à 01:42.
Pas besoin d'un papier de recherche pour cela, la notion de type somme c'est du niveau licence en mathématiques : c'est la somme disjointe d'ensemble (définie par une disjonction exclusive) qui est la notion jumelle du produit cartésien (type produit défini par une conjonction). Il n'y a rien de hautement sophistiqué là-dedans. C'est bien pour cela que je m'étonne de leur absence.
D'ailleurs, outre cette représentation dynamique des types, vous avez d'autres types sommes dans le langage. Si j'ai bien compris, la valeur
nilpeut être affectée à n'importe quel type, ce qui fait qu'en réalité vous ne manipulez que des types options, qui est un type somme : c'est le type1 + Apour tout typeA. Ce qui fait que lorsque vous avez des fonctions qui peuvent retourner une erreur, en renvoyant une paire, vous retournez un type produit de la forme suivante :(1 + A) * (1 + B) = 1 + A + B + A*B, où l'on voit les 4 cas à gérer que déplorait Colin Pitrat dans son premier commentaire. Là où, avec un type somme de résultat, il n'y a que les deux casA + B.Et ce n'est pas équivalent, même dans les faits. Cela l'est tout autant que Platon définissant l'homme comme un bipède sans plumes, et Diogène le cynique de le rayer en se promenant avec un poulet déplumé tout en haranguant la foule d'un « Voici un homme ! ».
Il y a d'autres types sommes infinis que l'on ne peut définir, en tant que tel, avec Go : celui des listes par exemples. Un type somme récursif, comme celui des listes, se développe en une somme infinie :
1 + A + A^2 + A^3 + ..., c'est-à-dire la liste vide, ou les listes à un élément, ou les listes à deux éléments, ou les listes à trois éléments...Tout ce que vous avez, c'est le type somme extensible que j'ai défini précédemment, qui est géré par le compilo et accolé dans une paire à toute valeur utilisant une interface. Puis vous faites du pattern matching dessus. Mais les seuls cas d'usage que j'ai vu, c'est avec l'interface vide pour palier le manque de polymorphisme dans le langage. L'exemple que tu m'as donné pour les arbres ne semble pas faire de d'analyse de cas sur la représentation dynamique des types, mais définir des arbres dans un langage qui n'a pas de type somme (directement définissables et accessibles au programmeur) mais que des types produits (ou struct ou enregistrements...) comme on peut le faire en C, C++, Java, Python, etc.
Ce que je veux dire c'est que l'outillage est là pour avoir une représentation dynamique des types, et que ce que j'ai fait à la main le compilo pourrait le faire automatiquement. Ce n'est pas la partie la plus dure, seulement je ne crois pas que quelqu'un y ait vu un quelconque intérêt à l'implémenter.
Je ne vois pas comment tu pourrais le faire aussi, simplement en bénéficiant d'un représentation dynamique des types. Soit la fonction est polymorphiquement paramétrique et là c'est très usuel en OCaml, soit le poylmorphisme est ad hoc et c'est le système des type classes (ou interface pour Go, mais le switch sur type ne sert à rien). Où a-t-on besoin d'une représentation dynamique des types ?
On peut faire de la sérialisation/déserialisation de manière type safe en OCaml, mais c'est ad hoc, il faut choisir son format. Les modules de la lib standard font cela de manière générique, ce qui ne peut être type safe. Même si l'on avait une représenation dynamique des types, je ne suis pas certain que l'on puisse réellement faire cela de manière générique et type safe.
Pour faire un
printftype safe il me semble qu'il faut les types dépendants, et en OCaml c'est implémenté via un GADT.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.