Algebraický datový typ

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