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.