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.
[^] # Re: Raisons d'essayer Rust
Posté par anaseto . En réponse au journal Retour d'expérience sur les langages de programmation. Évalué à 4. Dernière modification le 16 novembre 2020 à 21:25.
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).
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.
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).
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.