Algebraický datový typ je složený datový typ umožňující skládání pomocí algebraických operací součtu a součinu. Příkladem součinu typů jsou datové záznamy a struktury:
record Person where name : String age : Int
Příkladem součtu typů je například monáda s prázdnou hodnotou:
data Maybe : (a : Type) -> Type where Nothing : Maybe a Just : a -> Maybe a
Součin typů odpovídá logické konjunkci a součet disjunkci, čehož lze využít v jazycích jako Agda, Coq nebo Idris k formální verifikaci kódu. Algebraické datové typy tvoří polookruh, je proto možné definovat nad nimi například operaci derivování.
Zobecněné algebraické datové typy
Některé jazyky, například Idris, Lean a OCaml, mají takzvané zobecněné algebraické typy, v nichž mohou mít datové konstruktory různé výsledné typy, například v Idrisu:
data Even : Nat -> Type where EvenZ : Even 0 EvenSS : Even n -> Even (2+n)
Stejný typ v Leanu vypadá takto: inductive Even : Nat -> Type where | zero : Even 0 | plus2 : Even n -> Even (n+2)
Zobecněné datové typy je také možné použití jako existenciální typy v heterogenních datových kolekcích.
Kategorie:Teorie typů Kategorie:Datové struktury Kategorie:Datové typy