Type algébrique de données

Un type algébrique est une forme de type de données composite[note 1], 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.

Exemple : type produit en OCaml :

On peut définir en langage OCaml le type d’une entrée de dictionnaire :

type dict_entry = string * int

let entry = ("clé", 37)

(* get_value : dict_entry -> int *)
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 2]. 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.

Exemple : structure en OCaml :

Toujours en OCaml, l’exemple précédent s’adapte ainsi :

type dict_entry = {
  key   : string ;
  value : int ;
}

let entry = { key = "clé" ; value = 37 }

(* get_value : dict_entry -> int *)
let get_value entry = entry.value
Exemple : structure en langage C :

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 issue de A ne puisse pas être confondue avec une valeur issue de 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 ι1 a et ι2 b (ι est la lettre grecque iota). Ces notations ι1 et ι2 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. Dans ι1 a, la valeur a est appelée l’argument du constructeur ι1.

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é.

Exemple : type somme en OCaml :

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

(* print : sum -> unit *)
let print = function
  | Int i   -> Printf.printf "%i" i
  | Float f -> Printf.printf "%f" f

Ici, les constructeurs sont nommés Int et Float.

Exemple : type « union » en langage C :

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 énuméré

Un type énuméré représente un ensemble fini, dont les éléments sont les différents constructeurs. Définir une fonction dessus revient à définir l’image de chaque élément, individuellement.

Exemple : type énuméré en OCaml :

On peut par exemple coder l’ensemble des quatre couleurs d’un jeu de cartes classique :

type couleur = Coeur | Carreau | Trefle | Pique

(* nom_de_la_couleur : couleur -> string *)
let nom_de_la_couleur = function
  | Coeur   -> "♥ cœur"
  | Carreau -> "♦ carreau"
  | Trefle  -> "♣ trèfle"
  | Pique   -> "♠ pique"
Exemple : type énuméré en langage C :

Cette fonctionnalité se traduit en langage C par le mot‐clé enum :

typedef enum { COEUR, CARREAU, TREFLE, PIQUE } couleur ;

char* nom_de_la_couleur (couleur c) {
	switch (c) {
		case COEUR   : return "♥ cœur" ;
		case CARREAU : return "♦ carreau" ;
		case TREFLE  : return "♣ trèfle" ;
		case PIQUE   : return "♠ pique" ;
	}
}

Type algébrique

Un type algébrique est une somme de produits, et généralise donc ces deux notions.

Ainsi, des cas spéciaux de types algébriques sont les types produits (un seul constructeur), les types sommes (un seul argument pour chaque constructeur) et les types énumérations (plusieurs constructeurs sans argument).

Exemple : type option et type résultat :

Les types options (en) sont des applications courantes de types algébriques. Ils permettent d’ajouter à un type donné une valeur spéciale, considérée comme « indéfinie » ou comme valeur d’erreur (l’équivalent de null dans certains langages de programmation), ce qui permet de définir des fonctions partielles de façon contrôlée.

La valeur spéciale est représentée par un constructeur None qui ne prend aucun argument, tandis que les valeurs du type à compléter sont enveloppées dans un constructeur Some (qui prend donc un argument de ce type).

type int_option = None | Some of int

(* division : int -> int -> int_option *)
let division x y =
  if y = 0 then
    None
  else
    Some (x / y)

On peut perfectionner le mécanisme en agrémentant le cas d’erreur d’un message de description (donnée de type string).

type int_result = Result of int | Error of string

(* division : int -> int -> int_result *)
let division x y =
  if y = 0 then
    Error "division by zero"
  else
    Result (x / y)

Polymorphisme

Dans les langages qui les supportent, les types algébriques peuvent être (paramétriquement) polymorphes, ce qui permet la programmation générique. Ainsi, la définition d’un type algébrique peut être paramétrée par des variables de types.

On peut alors définir des fonctions génériques agissant sur de tels types polymorphes.

Exemple : type option polymorphe :

On peut rendre polymorphe la définition du type option vue précédemment. Ça s’écrit ainsi en langage OCaml (où 'a dénote une variable de type) :

type 'a option = None | Some of 'a

(** Utilisation d’instances du type polymorphe : **)

(* int_division : int -> int -> int option *)
let int_division x y =
  if y = 0 then
    None
  else
    Some (x / y)

(* float_division : float -> float -> float option *)
let float_division x y =
  if y = 0.0 then
    None
  else
    Some (x /. y)

(** Définition d’une fonction générique : **)

(* get_value : 'a -> 'a option -> 'a *)
let get_value default_value optional_value =
  match optional_value with
  | None       -> default_value
  | Some value -> value

Type algébrique généralisé

Récursivité

Listes

Un des exemples les plus importants de type algébrique est le type liste, défini de façon récursive 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.

Toutes les opérations sur les listes se définissent alors par récurrence, en utilisant le filtrage par motif. Par exemple, pour calculer la longueur d’une liste :

  • la longueur de la liste vide (Nil) est zéro,
  • et la longueur d’une liste de la forme Cons x suite est un plus la longueur de la liste suite.
Exemple : type liste en OCaml :

Cette définition se traduit ainsi en langage OCaml :

type 'a list =
  | Nil
  | Cons of 'a * 'a list

let list1234 = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil)))

let rec length = function
  | Nil      -> 0
  | Cons x s -> 1 + length s

Arbres

Les types algébriques permettent également de définir des structures d’arbres. Un arbre binaire peut se construire au moyen de deux constructeurs :

  • Leaf e qui désigne une feuille d’étiquette e,
  • et Node e g d qui désigne un nœud interne d’étiquette e, de fils gauche g et de fils droit d.

Par exemple,

Node 1
  (Node 2
    (Leaf 4)
    (Node 5
      (Leaf 6)
      (Leaf 7)
    )
  )
  (Leaf 3)

est l’arbre suivant :

    1
   / \
  2   3
 / \
4   5
   / \
  6   7

Comme pour les listes, les opérations sur les arbres se définissent par récurrence. Par exemple, pour calculer la hauteur d’un arbre :

  • la hauteur d’une feuille est un,
  • et la hauteur d’un nœud interne est un plus le maximum de la hauteur de ses deux fils.
Exemple : type arbre binaire en OCaml :

Cette définition se traduit ainsi en langage OCaml :

type tree =
  | Leaf of int 
  | Node of tree * int * tree

let my_tree = Node 1 (Node 2 (Leaf 4) (Node 5 (Leaf 6) (Leaf 7))) (Leaf 3)

let rec height = function
  | Leaf e     -> 1
  | Node e l r -> 1 + max (height l) (height r)

Abstraction

Un type algébrique peut être abstrait : il suffit pour ça de ne pas exposer sa structure interne (ses constructeurs et leurs divers champs). Ainsi, il ne peut être manipulé que par les fonctions prévues à cet effet, et son implémentation peut être changée.

C’est une technique fréquente car les types algébriques permettent de réaliser des structures de données complexes.

Voir aussi

Notes & références

Notes

  1. C’est‐à‐dire un type formé en combinant d’autres types plus simples.
  2. 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 type string * 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’expression entry.value permet seulement de déduire que la structure de entry 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.

Read other articles:

Robot ChickenGenreKomedi sketsa, parodi, komedi hitamPembuatSeth GreenMatthew SenreichPengisi suaraSeth GreenVariousLagu pembukaRobot Chicken oleh Les ClaypoolLagu penutupThe Gonk oleh Herbert ChappellPenata musikMichael SubyNegara asalAmerika SerikatJmlh. musim11Jmlh. episode220 (dan11 episode khusus) (daftar episode)ProduksiProduser eksekutifSeth GreenMatthew SenreichAlex BulkleyCorey CampodonicoJohn Harvatine IVEric TownerGeoff JohnsFor Williams Street:Keith CroffordMike LazzoDurasi11

 

Automatischer Belichtungsmesser Analoger Handbelichtungsmesser Practos II, optischer Belichtungsmesser; der Belichtungsmesser arbeitet rein optisch, die Belichtung wird auf einer optischen Skala ermittelt, wobei der Belichtungswert dem angezeigten Wert entspricht, der gerade noch sichtbar ist. Skala eines optischen Belichtungsmessers, ähnlich dem oben gezeigten Practos II Ein Belichtungsmesser ist ein Fotometer und dient in der Fotografie oder in der Filmfotografie dazu, die Helligkeit des M...

 

Наступ на Менаку Війна в Малі Дата: березень 8, 2022 - травень 2023 Місце: Округ Менака, Малі Результат: Перемога Ісламської держави Територіальні зміни: Регіон Менака (окрім міста Менака) повністю перейшов під контроль Ісламської держави Сторони CSP-PSD Рух Визволення Азаваду Гр...

Чідл — термін, який має кілька значень. Ця сторінка значень містить посилання на статті про кожне з них.Якщо ви потрапили сюди за внутрішнім посиланням, будь ласка, поверніться та виправте його так, щоб воно вказувало безпосередньо на потрібну статтю.@ пошук посилань саме...

 

Public community college in San Mateo, California, United States This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: College of San Mateo – news · newspapers · books · scholar · JSTOR (April 2013) (Learn how and when to remove this template message) College of San MateoMottoGateway to AchievementTypePublic commu...

 

Keuskupan Agung TurkuTurun arkkihiippakuntaÅbo ärkestiftGereja Lutheran Injili Finlandia Katedral TurkuLokasiNegaraFinlandiaProvinsi gerejawiTurku & FinlandiaMetropolitUskup Agung Turku & FinlandiaDekanat9InformasiDenominasiGereja Lutheran Injili FinlandiaKatedralKatedral TurkuKepemimpinan kiniUskup AgungTapio LuomaSufraganKaarlo KallialaSitus webwww.arkkihiippakunta.fi Keuskupan Agung Turku (bahasa Finlandia: Turun arkkihiippakunta, bahasa Swedia: Åbo ärkestift), yan...

Type of metamorphic rock This article is about the rock. For the toy, see Marble (toy). For other uses, see Marble (disambiguation). MarbleMetamorphic rockCarrara marble quarry in ItalyCompositionMostly calcite or dolomitePhysical CharacteristicsFabricTypically not foliatedRelationshipsProtolithscarbonate minerals, Limestone, Dolomite Marble is a metamorphic rock consisting of carbonate minerals that recrystallize under the influence of heat, pressure, and aqueous solutions (most commonly cal...

 

Intercollegiate sports teams of the University of Michigan Michigan WolverinesUniversityUniversity of MichiganConferenceBig Ten (primary)CWPA (women's water polo)NCAADivision I (FBS)Athletic directorWarde ManuelLocationAnn Arbor, MichiganVarsity teams29 (14 men's and 15 women's)Football stadiumMichigan StadiumBasketball arenaCrisler CenterIce hockey arenaYost Ice ArenaBaseball stadiumRay Fisher StadiumSoftball stadiumAlumni Field at The Wilpon ComplexSoccer stadiumU-M Soccer StadiumLacro...

 

2014 Nepali film by Ram Babu Gurung KabaddiTheatrical release posterNepaliकबड्डी Directed byRam Babu GurungWritten byRam Babu GurungProduced byRaunak Bikram Kandel Nischal BasnetSunil RauniyarStarringDayahang RaiNischal BasnetRishma GurungRajan KhatiwadaBuddhi TamangBijay BaralCinematographyPurushottam PradhanEdited byNibesh ShresthaMusic byAadha Sur Sound Design,Film Mix Uttam Neupane Release dates 25 April 2014 (2014-04-25) (Nepal and worldwide) Running time12...

Atlas Maritime Ltd.TypePrivateIndustryShipping, Oil Transportation and Commodities TransportationFounded(2004 (2004))FounderLeon PatitsasHeadquartersAthens, GreeceArea servedWorldwideKey peopleLeon Patitsas (CEO)Dimitrios Moutsis (General manager)Harris Takakis (Legal Counsel)Chris Zenios (CFO),ProductsOil tankers, dry bulkersNumber of employees285 (2017)WebsiteAtlas Maritime Atlas Maritime is an international shipping company with a fleet of tanker vessels engaged in the worldwide trans...

 

This article may require copy editing for grammar, style, cohesion, tone, or spelling. You can assist by editing it. (October 2023) (Learn how and when to remove this template message)This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Radha Ramana – news · newspapers · books · scholar · JSTOR (October 2023) (Le...

 

Indians in TanzaniaWatanzania wenye asili ya Kihindi (Swahili)Total populationc. 60,000 (2015)[1][a]Regions with significant populationsDar es Salaam, ZanzibarLanguagesOdia,[2] Punjabi, Sindhi, Gujarati, Telugu, Tamil, Kutchi, Kiswahili, English, HindiReligionIslam, Hinduism, Zoroastrianism, Sikhism; significant minorities ChristianityRelated ethnic groupsPIO, NRI and Desia.^ includes about 10,000 expatriates Indian Prime Minister Narendra Modi meets members of Indian com...

The topic of this article may not meet Wikipedia's notability guidelines for products and services. Please help to demonstrate the notability of the topic by citing reliable secondary sources that are independent of the topic and provide significant coverage of it beyond a mere trivial mention. If notability cannot be shown, the article is likely to be merged, redirected, or deleted.Find sources: Vrio Corp. – news · newspapers · books · scholar · JSTOR...

 

Elisabeth van Beieren kan verwijzen naar: Elisabeth van Beieren (1227-1273), echtgenote van Koenraad IV Elisabeth van Beieren (1306-1330), echtgenote van Otto van Oostenrijk Elisabeth van Beieren (1329-1402), echtgenote van Cangrande II della Scala van Verona en Ulrich van Württemberg Elisabeth van Beieren (1350-1415), dochter van Willem V van Holland Elisabeth van Beieren (1383-1442), echtgenote van Frederik I van Brandenburg Elisabeth van Beieren (1443-1484), echtgenote van Ernst van Sakse...

 

City in Hawaii, United States City in Hawaii, United StatesMililaniCityLocation in Honolulu County and the state of HawaiiMililaniLocation in HawaiiCoordinates: 21°26′45″N 158°0′51″W / 21.44583°N 158.01417°W / 21.44583; -158.01417Country United StatesState HawaiiCity & County HonoluluArea • Total6.6 sq mi (17.1 km2) • Land6.6 sq mi (17.1 km2) • Water0.0 sq mi (0.0 ...

Species of fish Gulf killifish Conservation status Least Concern (IUCN 3.1)[1] Scientific classification Domain: Eukaryota Kingdom: Animalia Phylum: Chordata Class: Actinopterygii Order: Cyprinodontiformes Family: Fundulidae Genus: Fundulus Species: F. grandis Binomial name Fundulus grandisBaird & Girard, 1853 Synonyms[2] Fundulus floridensis Girard, 1859 Fundulus pallidus Evermann, 1892 The Gulf killifish (Fundulus grandis) is one of the largest members of the g...

 

Park in north-west London This article is about the park in north-west London. For the district, see Primrose Hill (district). For other uses, see Primrose Hill (disambiguation). Primrose HillThe view of London from the top of Primrose HillThe location of Primrose Hill in LondonTypePublic ParkLocationLondon Borough of Camden, London, UKNearest cityLondonOS gridTQ282838Coordinates51°32′23″N 0°09′39″W / 51.5396°N 0.1608°W / 51.5396; -0.1608Area25.18 hect...

 

This article is about the super heroine. For other uses, see Rainbow Girl (disambiguation). This article relies excessively on references to primary sources. Please improve this article by adding secondary or tertiary sources. Find sources: Rainbow Girl – news · newspapers · books · scholar · JSTOR (May 2016) (Learn how and when to remove this template message) Comics character Rainbow GirlRainbow Girl as depicted in Action Comics #862 (April 2008). Ar...

Calle Hatun Rumiyoq Cusco, Perú Perú Hatun RumiyoqDatos de la rutaTipo PeatonalInauguración IncanatoAncho de calzada 3 metrosLongitud 141 metrosOtros datosPrincipales puntos turísticos Piedra de los doce ángulosPalacio ArzobispalOrientación • Noreste Calle ChoquechakaCuesta de San Blas • Suroeste Calle Herrajes/Calle PalacioCalle TriunfoLugaresDistrito que atraviesa CuscoUbicación 13°30′58″S 71°58′35″O / -13.515984, -71.976275Siguientes ruta...

 

Saman Sampul Saman, dari lukisan Dia Seperti Sedang Menuliskan Sesuatu, karya Agus SuwagePengarangAyu UtamiPerancang sampulLukisan:Agus SuwageDesain:Sijo SudarsonoNegaraIndonesiaBahasabahasa IndonesiaPenerbitKepustakaan Populer GramediaTanggal terbitApril 1998 (cetakan pertama Indonesia)Jenis mediasampul lunakHalaman208 halamanISBNISBN 979-9023-17-3Diikuti olehLarung (2001)  Saman adalah novel pertama karya Ayu Utami yang diterbitkan oleh Kepustakaan Populer Gramedia ...

 

Strategi Solo vs Squad di Free Fire: Cara Menang Mudah!