Les types de données algébriques de Haskell

Question

Je suis en train d'essayer de comprendre pleinement tous les concepts de Haskell.

En quoi les types de données algébriques sont-ils similaires aux types génériques, par exemple, en C# et Java? Et en quoi sont-ils différents? En quoi sont-ils si algébriques?

Je connais l'algèbre universelle et ses anneaux et champs, mais je n'ai qu'une vague idée de comment les types de Haskell fonctionnent.

Answer 1

Les types de données algébriques de Haskell sont ainsi nommés car ils correspondent à une algèbre initiale en théorie des catégories, nous donnant quelques lois, quelques opérations et quelques symboles à manipuler. Nous pouvons même utiliser une notation algébrique pour décrire des structures de données régulières, où:

• + représente des types somme (unions disjointes, par ex. Either).
• • représente des types produit (par ex. structs ou tuples)
• X pour le type singleton (par ex. data X a = X a)
• 1 pour le type unité ()
• et μ pour le point fixe le plus petit (par ex. types récursifs), généralement implicite.

avec une notation additionnelle:

• X² pour X•X

En fait, on pourrait dire (suivant Brent Yorgey) qu'un type de données Haskell est régulier s'il peut être exprimé en termes de 1, X, +, •, et un point fixe le moins.

Avec cette notation, nous pouvons décrire de manière concise de nombreuses structures de données régulières:

• Unités: data () = ()

  1

• Options: data Maybe a = Nothing | Just a

  1 + X

• Listes: data [a] = [] | a : [a]

  L = 1+X•L

• Arbres binaires: data BTree a = Empty | Node a (BTree a) (BTree a)

  B = 1 + X•B²

D'autres opérations sont possibles (extraits du document de Brent Yorgey, répertoriés dans les références):

• Expansion: déplier le point fixe peut être utile pour réfléchir aux listes. L = 1 + X + X² + X³ + ... (c'est-à-dire, les listes sont soit vides, soit elles ont un élément, ou deux éléments, ou trois, ou ...)

• Composition, ◦, étant donnés les types F et G, la composition F ◦ G est un type qui construit des "structures F faites de structures G" (par ex. R = X • (L ◦ R) ,où L sont les listes, est un arbre en roseaux.

• Différenciation, la dérivée d'un type de données D (donnée sous forme de D') est le type des structures D avec un seul "trou", c'est-à-dire, un emplacement distingué ne contenant aucune donnée. Cela satisfait étonnamment les mêmes règles que pour la différenciation en calcul:

  1′ = 0

  X′ = 1

  (F + G)′ = F' + G′

  (F • G)′ = F • G′ + F′ • G

  (F ◦ G)′ = (F′ ◦ G) • G′

---

Références:

• Species and Functors and Types, Brent A. Yorgey, Haskell’10, 30 septembre 2010, Baltimore, Maryland, États-Unis
• Clowns to the left of me, jokers to the right (Dissecting Data Structures), Conor McBride POPL 2008

Answer 2

Les "Types de Données Algébriques" en Haskell prennent en charge le polymorphisme paramétrique complet, qui est le nom le plus techniquement correct pour les génériques, comme un exemple simple le type de données de liste :

 data List a = Cons a (List a) | Nil

Est équivalent (autant que possible, et en ignorant l'évaluation non stricte, etc) à

 class List {
     class Cons : List {
         a head;
         List tail;
     }
     class Nil : List {}
 }

Bien sûr, le système de type de Haskell permet des utilisations plus ... intéressantes des paramètres de type mais ceci est juste un exemple simple. En ce qui concerne le nom "Type Algébrique", je n'ai honnêtement jamais été tout à fait sûr de la raison exacte pour laquelle ils ont été nommés ainsi, mais j'ai supposé que c'était en raison des fondements mathématiques du système de type. Je pense que la raison se résume à la définition théorique d'un ADT étant le "produit d'un ensemble de constructeurs", cependant cela fait quelques années que j'ai quitté l'université donc je ne me souviens plus des détails.

[Edit : Merci à Chris Conway d'avoir souligné mon erreur stupide, les ADT sont bien sûr des types somme, les constructeurs fournissant le produit/tuple de champs]

Answer 3

Dans l'algèbre universelle un algèbre consiste en ensembles d'éléments (pensez à chaque ensemble comme l'ensemble de valeurs d'un type) et des opérations, qui mappent des éléments vers d'autres éléments.

Par exemple, supposez que vous avez un type d'"éléments de liste" et un type de "listes". Comme opérations vous avez la "liste vide", qui est une fonction à 0 arguments retournant une "liste", et une fonction "cons" qui prend deux arguments, un "élément de liste" et une "liste", et produit une "liste".

À ce stade, il y a de nombreuses algèbres qui correspondent à cette définition, car deux choses indésirables peuvent se produire:

• Il pourrait y avoir des éléments dans l'ensemble "liste" qui ne peuvent pas être construits à partir de la "liste vide" et de l'opération "cons", une sorte de "junk". Il pourrait s'agir de listes commençant par un élément tombé du ciel, de boucles sans commencement, ou de listes infinies.

• Les résultats de "cons" appliqué à différents arguments pourraient être égaux, par exemple, ajouter un élément à une liste non vide pourrait être égal à la liste vide. Cela s'appelle parfois "confusion".

Une algèbre qui ne présente aucune de ces propriétés indésirables est appelée algèbre initiale, et c'est le sens voulu du type de données abstrait.

Le nom initial provient de la propriété qu'il y a exactement un homomorphisme de l'algèbre initiale vers une algèbre donnée. Essentiellement vous pouvez évaluer la valeur d'une liste en appliquant les opérations dans l'autre algèbre, et le résultat est bien défini.

Cela devient plus compliqué pour les types polymorphes ...

Answer 4

Une raison simple pour laquelle ils sont appelés algébriques; il existe à la fois des types de somme (disjonction logique) et des types de produit (conjonction logique). Un type de somme est un union discriminée, par exemple:

data Bool = False | True

Un type de produit est un type avec plusieurs paramètres:

data Pair a b = Pair a b

En O'Caml, le "produit" est rendu plus explicite:

type 'a 'b pair = Pair of 'a * 'b

Answer 5

Les types de données de Haskell sont appelés "algébriques" en raison de leur connexion aux algèbres initiales catégoriques. Mais c'est le chemin de la folie.

@olliej: Les ADT sont en fait des types "somme". Les tuples sont des produits.