Les types de données algébriques de Haskell

Haskell's types de données algébriques sont nommés tels car ils correspondent à un algèbre initiale dans la 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 exemple Either ).
• • représente des types de produits (par exemple des structures ou des tuples)
• X pour le type singleton (p.ex. data X a = X a )
• 1 pour le type d'unité ()
• et μ pour le point le moins fixe (p.ex. types récursifs), généralement implicite.

avec mention supplémentaire:

• X² pour X•X

en fait, vous pourriez dire (suivant Brent Yorgey) qu'un type de données Haskell est régulier si elle peut être exprimée en termes de 1 , X , + , • , et un point moins fixe.

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²

autres opérations les références):

• Expansion: le déploiement du point de repère peut être utile pour réfléchir à des listes. L = 1 + X + X² + X³ + ... (c'est-à-dire que les listes sont vides, ou qu'elles ont un ou deux éléments, ou trois, ou ...)

• Composition, ◦ , étant donné les types F et G , la composition F ◦ G est un type qui construit des "structures en F constituées par des structures en G" (p.ex. R = X • (L ◦ R) ,où L est des listes, est un rosier.

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

  1′ = 0

  X′ = 1

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

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

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

références:

• "15191240920 les Espèces et les Foncteurs et les Types , Oh Mon dieu!, Brent A. Yorgey, Haskell '10, 30 septembre 2010, Baltimore, Maryland ,USA
• Clowns à ma gauche, jokers à ma droite (Dissecting Data Structures) , Conor McBride POPL 2008

In algèbre universelle un algèbre se compose de quelques ensembles d'éléments (pensez à chaque définir comme l'ensemble des valeurs d'un type) et certaines opérations, qui font correspondre des éléments à des éléments.

par exemple, supposons que vous ayez un type de" list elements " et un type de "listes". Comme opérations vous avez la "liste vide", qui est un 0-argument fonction retournant une "liste", et un "contre" fonction qui prend deux arguments, liste élément" et une "liste", et de produire une "liste".

à ce point il y a beaucoup d'algèbres qui correspondent à la description, comme deux choses indésirables peuvent arriver:

• il pourrait y avoir des éléments dans l'ensemble "list" qui ne peuvent pas être construits à partir de la "liste vide" et les "contre" soi-disant "indésirable". Ça pourrait être des listes à partir d'un élément tombé du ciel., ou des boucles sans commencement, ou infini listes.

• Les résultats de "cons" appliquée à différents arguments pourraient être égale, par exemple, placer un élément dans une liste non vide pourrait être égale à la liste vide. C'est ce qu'on appelle parfois la "confusion".

une algèbre qui n'a aucune de ces propriétés indésirables est appelée initial , et c'est la signification prévue du type de données abstraites.

le nom dérive initiale 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 de dans l'autre algèbre, et le résultat est bien défini.

c'est plus compliqué pour les types polymorphes ...

une raison simple pour laquelle on les appelle algébriques; il y a à la fois des types de somme (disjonction logique) et de produit (conjonction logique). Un type de Somme est un syndicat discriminé, E. g:

data Bool = False | True

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

data Pair a b = Pair a b

O'Caml "produit" est 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 à algèbres initiales catégoriques . Mais cette voie est la folie.

@olliej: les ADT sont en fait des types "sum". Les Tuples sont des produits.

@Timbo:

vous avez fondamentalement raison sur le fait qu'il s'agit en quelque sorte d'une classe d'arbre abstrait avec trois classes dérivées (Empty, Leaf, and Node), mais vous devriez également appliquer la garantie que quelqu'un utilisant votre classe D'arbre ne peut jamais ajouter de nouvelles classes dérivées, puisque la stratégie pour utiliser le type de données D'arbre est d'écrire du code qui change à l'exécution basée sur le type de chaque élément dans l'arbre (et l'ajout de nouveaux types dérivés briserait le code existant). Vous peut en quelque sorte imaginer que cela devienne désagréable en C# ou C++, mais en Haskell, ML, et OCaml, c'est au centre de la conception du langage et de la syntaxe de sorte que le style de codage le supporte d'une manière beaucoup plus commode, via l'appariement de motifs.

ADT (types de Somme) sont aussi en quelque sorte comme unions marquées ou variantes en C ou C++.

question ancienne, 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 solutions de rechange, il est possible de procéder à un appariement exhaustif des motifs fondés sur les cas.

pour moi, le concept des types de données algébriques d'Haskell ressemblait toujours à du polymorphisme dans les langues OO comme C#.

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

data Tree = Empty 
          | Leaf Int 
          | Node Tree Tree

ceci pourrait être implémenté dans C# comme une classe de base TreeNode, avec une classe de feuille dérivée et une classe treenodewithchildren dérivée, et si vous voulez même une classe de EmptyNode dérivée.

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