Types de données algébriques de Haskell

https://stackoverflow.com/questions/16770

08-06-2019
|

Question

J'essaie 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 ?Qu'ont-ils de si algébrique, de toute façon ?

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

La solution

"Types de données algébriques" dans le support Haskell polymorphisme paramétrique complet, qui est le nom le plus techniquement correct pour les génériques, à titre d'exemple simple, le type de données list :

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

Est équivalent (dans la mesure du possible, et en ignorant les évaluations non strictes, etc.) à

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

Bien sûr, le système de types de Haskell permet plus...utilisation intéressante des paramètres de type mais ce n’est qu’un exemple simple.En ce qui concerne le nom "Type algébrique", honnêtement, je n'ai jamais été entièrement sûr de la raison exacte pour laquelle ils sont nommés ainsi, mais j'ai supposé que cela était dû aux fondements mathématiques du système de types.je croire que la raison se résume à la définition théorique d'un ADT comme étant le "produit d'un ensemble de constructeurs", mais cela fait quelques années que j'ai échappé à l'université donc je ne me souviens plus des détails.

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

Autres conseils

Haskell types de données algébriques sont nommés ainsi puisqu'ils correspondent à un 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 la notation algébrique pour décrire des structures de données régulières, où :

+ représente les types de somme (unions disjointes, par ex. Either).
• représente les types de produits (par ex.structures ou tuples)
X pour le type singleton (par ex. data X a = X a)
1 pour le type d'unité ()
et μ pour le point le moins fixe (par ex.types récursifs), généralement implicites.

avec quelques notations supplémentaires :

X² pour X•X

En fait, on pourrait dire (à la suite de 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 le moins ﬁxe.

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

Unités: data () = ()

1
Possibilités : 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 valables (tirées de l'article de Brent Yorgey, répertoriées 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 que les listes sont soit vides, soit comportant un élément, ou deux éléments, ou trois, ou ...)
Composition, ◦, types donnés F et G, la composition F ◦ G est un type qui construit des « structures F faites à partir de structures G » (par ex. R = X • (L ◦ R) ,où L C'est des listes, c'est un rosier.
La différenciation, la dérivée d'un type de données D (donné comme D') est le type de structures D avec un seul « trou », c'est-à-dire un emplacement distinctif ne contenant aucune donnée.Cela satisfait étonnamment aux 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′

Les références:

Espèces, foncteurs et types, Oh mon Dieu !, Brent A.Yorgey, Haskell’10, 30 septembre 2010, Baltimore, Maryland, États-Unis
Des clowns à ma gauche, des farceurs à droite (Dissection des structures de données), Conor McBride POPL 2008

Dans algèbre universelle un algèbre se compose d’un ensemble d’éléments (considérez chaque ensemble comme l’ensemble des valeurs d’un type) et certaines opérations, qui associent des éléments à des éléments.

Par exemple, supposons que vous ayez un type d’éléments de liste et un type de « listes ».En tant qu’opérations, vous avez la « liste vide », qui est un argument 0 une fonction renvoyant une « liste », et une fonction « cons » qui prend deux arguments, un « élément de liste » et une « liste », et produire une « liste ».

À ce stade, il existe de nombreuses algèbres qui correspondent à la description, car deux choses indésirables peuvent se produire :

Il pourrait y avoir des éléments dans l'ensemble "Liste" qui ne peut pas être construit à partir de la "liste vide" et de "l'opération contre", ce que l'on appelle "Junk".Il pourrait s'agir de listes à partir d'un élément qui est tombé du ciel, ou de boucles sans début, ou listes infinies.
Les résultats de "CONS" appliqués à différents arguments pourraient être égaux, par exempleLe fait qu'un élément d'une liste non vide pourrait être égal à la liste vide.C'est ce qu'on appelle parfois « confusion ».

Une algèbre qui n’a aucune de ces propriétés indésirables est appeléeinitial, et c'est la signification voulue du type de données abstrait.

L’initiale du nom dérive de la propriété qu’il y a exactement un homomorphisme de l’algèbre initiale à 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...

Une raison simple pour laquelle ils sont appelés algébriques ;il existe à la fois des types somme (disjonction logique) et produit (conjonction logique).Un type somme est une 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

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

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

Les types de données de Haskell sont appelés « algébriques » en raison de leur connexion avec algèbres initiales catégorielles.Mais c’est là que réside la folie.

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

@Timbo :

Vous avez fondamentalement raison de dire qu'il s'agit d'une sorte de classe Tree abstraite avec trois classes dérivées (Empty, Leaf et Node), mais vous devrez également faire respecter la garantie que quelqu'un utilisant votre classe Tree ne pourra jamais ajouter de nouvelles classes dérivées. , puisque la stratégie d'utilisation du type de données Tree consiste à écrire du code qui change au moment de l'exécution en fonction du type de chaque élément de l'arborescence (et l'ajout de nouveaux types dérivés casserait le code existant).Vous pouvez en quelque sorte imaginer que cela devienne désagréable en C# ou C++, mais en Haskell, ML et OCaml, cela est au cœur de la conception et de la syntaxe du langage, donc le style de codage le prend en charge de manière beaucoup plus pratique, via la correspondance de modèles.

Les ADT (types de somme) sont aussi un peu comme syndicats tagués ou types de variantes en C ou C++.

vieille question, mais personne n'a mentionné la nullité, qui est un aspect important des types de données algébriques, peut-être l'aspect le plus important.Étant donné que chaque valeur est l'une des alternatives, une correspondance exhaustive de modèles basée sur des cas est possible.

Pour moi, le concept des types de données algébriques de Haskell a toujours ressemblé au polymorphisme dans les langages OO comme C#.

Regardez l'exemple de http://en.wikipedia.org/wiki/Algebraic_data_types:

data Tree = Empty 
          | Leaf Int 
          | Node Tree Tree

Cela pourrait être implémenté en C# en tant que classe de base TreeNode, avec une classe Leaf dérivée et une classe TreeNodeWithChildren dérivée, et si vous souhaitez même une classe EmptyNode dérivée.

(OK, je sais, personne ne ferait jamais ça, mais au moins tu pourrais le faire.)

Licencié sous: CC-BY-SA avec attribution

Non affilié à StackOverflow