« Type algébrique de données » : différence entre les versions
plan |
|||
Ligne 57 : | Ligne 57 : | ||
}} |
}} |
||
{{article |
{{article détaillé|enregistrement (programmation informatique)}} |
||
=== Type somme === |
=== Type somme === |
Version du 20 août 2016 à 21:40
Un type algébrique est une forme de type de données qui combine les fonctionnalités des types produits (n‐uplets ou enregistrements) et des types sommes (union disjointe). Combinée à la récursivité, elle permet d’exprimer les données structurées telles que les listes et les arbres.
Définitions
Type produit
Le type produit de deux types A et B est l’analogue en théorie des types du produit cartésien ensembliste et est noté A × B. C’est le type des couples dont la première composante est de type A et la seconde de type B. Deux fonctions canoniques lui sont associées, appelées projections, donnant la valeur de chaque composante.
On peut définir en langage OCaml le type d’une entrée de dictionnaire :
type dict_entry = string * int
let entry = ("clé", 37)
let get_value (key, value) = value
Le produit se généralise naturellement à un nombre quelconque d’opérandes, pour donner des types de n‐uplets. Dans le cas particulier du produit vide, le type des 0‐uplets est nommé type unité et noté 1 : c’est l’élément neutre du produit et il contient une unique valeur, souvent notée ().
Des considérations pratiques amènent souvent à nommer les composantes[note 1]. Dans ce contexte, le type est souvent appelé structure et ses valeurs des enregistrements ; les composantes sont appelées membres, et la projection selon le membre m
s’écrit avec une notation suffixe .m
.
Toujours en OCaml, l’exemple précédent s’adapte ainsi :
type dict_entry = {
key : string ;
value : int ;
}
let entry = { key = "clé" ; value = 37 }
let get_value entry = entry.value
Cette fonctionnalité se traduit en langage C par le mot‐clé struct
(en) :
typedef struct {
char* key ;
int value ;
} dict_entry ;
dict_entry entry = { .key = "clé", .value = 37 } ;
int get_value (dict_entry entry) {
return entry.value ;
}
Type somme
Le type somme de deux types A et B est l’analogue en théorie des types de l’union disjointe ensembliste et est noté A + B. Il représente un type contenant toutes les valeurs de chacun des deux types A et B, de telle sorte qu’une valeur de type A ne puisse pas être confondue avec une valeur de type B (même si A = B).
En théorie des ensembles, on représenterait la somme par l’ensemble {1}×A ∪ {2}×B ; la première composante (1 ou 2) d’un tel objet est une étiquette qui indique si cet objet se trouve dans le bras de gauche (A) ou dans le bras de droite (B) de la somme. Les analogues en théorie des types des expressions (1, a) et (2, b) sont souvent notés ι₁ a et ι₂ b. Ces notations ι₁ et ι₂ peuvent être vues comme des fonctions injectives, respectivement de A dans A + B et de B dans A + B, qui permettent de construire les valeurs de la somme, d’où leur nom de constructeurs.
Traiter des valeurs d’un type somme requiert un raisonnement par cas, nommé dans ce contexte filtrage par motif. Chaque bras — qu’on reconnaît par son constructeur et dont on peut récupérer la valeur puisque ce constructeur est injectif — fait l’objet d’un cas séparé.
On peut définir on OCaml l’union disjointe des nombres entiers et des nombres flottants et définir par filtrage une fonction sur cette union :
type sum = Int of int | Float of float
let print = function
| Int i -> Printf.printf "%i" i
| Float f -> Printf.printf "%f" f
Ici, les constructeurs sont nommés Int
et Float
.
Cette fonctionnalité s’approxime en langage C avec le mot clé union
(en) à condition d’y adjoindre une étiquette, mais cela n’offre pas les mêmes garanties (on peut lire et modifier un objet du type somme en faisant fi de son étiquette — quitte à provoquer des bugs) :
typedef struct {
enum { INT, FLOAT } tag ;
union {
int i ;
float f ;
} ;
} sum_t ;
void print (sum_t x) {
if (x.tag == INT)
printf("%i", x.i) ;
else if (x.tag == FLOAT)
printf("%f", x.f) ;
}
La somme se généralise naturellement à un nombre quelconque d’opérandes. Dans le cas particulier de la somme vide, le type est nommé type vide et noté 0 : c’est l’élément neutre de la somme (et élément absorbant du produit) et il ne contient aucune valeur.
Type algébrique
Un type algébrique est une somme de produits, et généralise donc ces deux notions.
C’est donc un type de données dont chaque valeur est un n‐uplet d'un certain type enveloppé dans un constructeur. Toutes les composantes enveloppées sont des arguments du constructeur. Par contraste avec d’autres types de données, le constructeur n'est pas exécuté et[évasif] la seule manière d'opérer sur les données est d'enlever le constructeur en utilisant le filtrage par motif.
Un des exemples les plus courants de type algébrique est le type liste, défini par deux constructeurs :
Nil
, aussi noté[]
, qui désigne la liste vide,- et
Cons
(abréviation de « constructeur »), aussi noté:
ou::
, qui désigne la combinaison d’un élément et d’une liste plus courte.
Par exemple, Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))
, aussi noté 1 : 2 : 3 : 4 : []
, est la liste constituée des quatre éléments 1, 2, 3, 4, dans cet ordre.
Des cas spéciaux de types algébriques sont des types produit (un seul constructeur) et les types énumération (plusieurs constructeurs sans argument). Les types algébriques sont une forme de type composite, c’est-à-dire un type formé en combinant plusieurs autres types.
Un type algébrique de données peut être aussi un type abstrait de données (sigle anglais : ADT) s'il est exporté à partir d'un module sans ses constructeurs. Les valeurs d'un tel type peuvent être manipulées seulement avec des fonctions définies dans le même module que le type lui-même.
En théorie des ensembles, l'équivalent d'un type algébrique de données est la réunion disjointe (ou somme ensembliste), une réunion dont les éléments communs sont en quelque sorte dupliqués. Formellement, les éléments dupliqués sont distingués par l’adjonction d’un marqueur (l'équivalent d'un constructeur) identifiant l’ensemble d’origine de l’élément. La construction est généralisée en rendant obligatoire le marqueur pour tous les éléments, même ceux dont le type pourrait être laissé implicite.
Un exemple
En Haskell, on peut définir un nouveau type algébrique de données, Tree
:
data Tree = Empty
| Leaf Int
| Node Tree Tree
ou dans la syntaxe OCaml :
type tree = Empty
| Leaf of int
| Node of tree * tree
Ici, Empty
, Leaf
et Node
sont des constructeurs.
De manière similaire à une fonction, un constructeur est appliqué aux arguments du type approprié, donnant une instance du type de données
auquel le constructeur appartient. Par exemple Leaf
a un type fonctionnel Int -> Tree
.
Cela signifie qu'étant donné un entier comme argument à Leaf
produit une valeur de type Tree
.
Comme Node
prend deux arguments du type Tree
lui-même, le type est type récursif.
Les opérations sur les types algébriques de données peuvent être définies par le filtrage par motif pour retrouver les
arguments. Par exemple, considérons une fonction pour calculer la profondeur d'une Tree
:
depth :: Tree -> Int
depth Empty = 0
depth (Leaf n) = 1
depth (Node l r) = 1 + max (depth l) (depth r)
Donc, un Tree
donné à la fonction depth
peut
être aussi construit pour chacun d'eux pour traiter tous les cas. Dans
les cas de Node
, le motif extrait les sous-arbres
l
et r
pour un traitement ultérieur.
Polymorphisme
Type algébrique généralisé
Récursivité
Voir aussi
Notes & références
Notes
- De structurel, le typage devient alors nominal. Dans le premier cas, l’expression d’un n‐uplet permet de déduire entièrement sa structure (par exemple,
("clé", 37)
est de typestring * int
) et déclarer le type est donc superflu. Dans le second cas, au contraire, l’expression ne suffit pas ({ key = "clé" ; value = 37 }
peut suivre la structure{ key : string ; value : int }
mais aussi{ value : int ; key : string }
— qui est différente —, et l’expressionentry.value
permet seulement de déduire que la structure deentry
contient un champ nommévalue
), et il faut donc déclarer les structures utilisées afin d’associer chaque nom de membre à une structure.
Références
- (en) Algebraic data type dans The Free On-line Dictionary of Computing, rédacteur en chef Denis Howe.