Qu'est-ce qu'une structure de données de type "somme et produit" ?

Question

A billet récent sur les Fusings de William Cook mentions :

Le point essentiel est que les structures d'Enso sont considérées de manière holistique comme des graphiques, et non comme des valeurs individuelles ou des structures de données traditionnelles de type "somme et produit".

Quelles sont les structures de données traditionnelles de type somme et produit auxquelles il fait référence ?

Answer 1

Quelles sont les structures de données traditionnelles de type somme et produit auxquelles il fait référence ?

Dans la théorie des types, les structures de données régulières peuvent être décrites en termes de sommes, de produits et de types récursifs. Cela conduit à une algèbre pour décrire les structures de données (et ce que l'on appelle les types de données algébriques ). Ces types de données sont courants dans les langages fonctionnels à typage statique, tels que ML ou Haskell.

Produits

Les produits peuvent être considérés comme le point de vue de la théorie des types sur les "structures" ou les "tuples".

Officiellement, PFPL, Ch 14 :

Le système binaire produit de deux types consiste en des paires ordonnées de valeurs, l'une provenant de de chaque type dans l'ordre spécifié. Les formes éliminatoires associées sont des projections, qui sélectionnent le premier et le deuxième composant d'une paire. Le produit nullaire, ou type d'unité, consiste uniquement en un "tuple nul" unique d'aucune valeur, et n'a pas de forme éliminatoire associée.

Sommes

Les types de sommes expriment le choix entre les variantes d'une structure de données. Ils sont parfois appelés "types d'union" (comme en C). De nombreux langages n'ont pas de notion de type somme.

PFPL, chapitre 15 :

La plupart des structures de données impliquent des alternatives telles que la distinction entre un feuille et un nœud intérieur dans un arbre, ou un choix dans la forme la plus extérieure d'un morceau d'abstraction. syntaxe abstraite. Il est important de noter que le choix détermine la structure de la valeur. Par exemple, les nœuds ont des enfants, mais pas les feuilles, et ainsi de suite. et ainsi de suite. Ces concepts sont exprimés par des types de somme, en particulier le type binaire binaire, qui offre le choix entre deux choses, et la somme nullaire, qui offre le choix entre aucune chose. un choix entre deux choses, et la somme nullaire, qui offre un choix entre aucune chose.

Types récursifs

Outre les produits et les sommes, nous pouvons introduire la récursivité, de sorte qu'un type peut être défini (partiellement) en termes de lui-même. Les arbres et les listes en sont de bons exemples.

 data List a = Empty | a : List a

 data Tree a = Nil | Node a (Tree a) (Tree a)

Algèbre des sommes, des produits et de la récursivité

Donnez un type, par exemple Int nous pouvons commencer à élaborer une notation pour les expressions algébriques qui décrivent les structures de données :

Une seule variable :

Int

Un produit de deux types (dénotant une paire) :

Int * Bool

Une somme de deux types (dénotant un choix entre deux types) :

Int + Bool

Et quelques constantes :

1 + Int

donde 1 est le type d'unité, () .

Une fois que vous pouvez décrire les types de cette manière, vous obtenez gratuitement des pouvoirs intéressants. Premièrement, une notation très concise pour décrire les types de données, deuxièmement, certains résultats transférés depuis d'autres algèbres (par exemple travaux de différenciation sur les structures de données ).

Exemples

Le type d'unité, data () = ()

Un tuple, le plus simple type de produit : data (a,b) = (a,b)

Un simple type de somme , data Maybe a = Nothing | Just a

et son alternative,

et un type récursif le type de listes chaînées : data [a] = [] | a : [a]

À partir de là, il est possible de construire des structures assez complexes en combinant des sommes, des produits et des types récursifs. Par exemple, la notation simple d'une liste de produits de sommes de produits : [(Maybe ([Char], Double), Integer)] donne lieu à des arbres assez compliqués :

---

Références

• Fondements pratiques de la programmation Language, Robert Harper, 2011, http://www.cs.cmu.edu/~rwh/plbook/book.pdf
• Introduction rapide à l'algèbre des types de données, http://blog.lab49.com/archives/3011 (Le lien semble être mort. Lien Internet Archive : http://web-old.archive.org/web/20120321033340/http://blog.lab49.com/archives/3011 )
• Espèces, foncteurs et types, Oh My !, Brent Yorgey, http://www.cis.upenn.edu/~byorgey/papers/species-pearl.pdf -- a une très bonne vue d'ensemble de l'algèbre, des types de données Haskell, et de la connexion avec espèces combinatoires des mathématiques.

Answer 2

Des réponses très détaillées ont déjà été données, mais, pour une raison ou une autre, elles ne mentionnent pas ce simple fait.

Les types de sommes sont appelés ainsi parce que le nombre de valeurs possibles d'un type de somme est le somme du nombre de valeurs des deux types sous-jacents. De même, pour les types de produits, le nombre de valeurs possibles est le produit.

Cela découle de la théorie des types qui définit un type comme un ensemble de valeurs.

data MySumType = Foo Bool | Bar Char
data MyProductType = Baz (Bool, Char)

• Bool est un ensemble de 2 valeurs.
• Char est un ensemble de 256 valeurs.
• MySumType est un ensemble de 2 + 256 valeurs.
• MyProductType est un ensemble de 2 * 256 valeurs.

Vous n'oublierez plus jamais lequel est lequel.

Answer 3

Il fait référence à la norme types de données algébriques des langages de programmation fonctionnels.

Exemples :

• Si a est du type A y b est du type B puis (a, b) est du type A x B qui est un type de produit .

• Un type de liste avec des valeurs de la forme Nil o Cons x xs est un type de somme .

Ensō met apparemment davantage l'accent sur les graphes que sur ces types algébriques arborescents.

Answer 4

Extrait des notes de cours pour le cours Coursera, "Programming Languages", proposé par l'Université de Washington :

"Pourquoi le produit et la somme ? C'est lié au fait qu'en algèbre booléenne, où 0 est faux et 1 est vrai, et fonctionne comme multiplier et ou fonctionne comme additionner."