Druh (teorie typů)

Druh je v teorii typů "typ typu". Druh konkrétních typů (např. čísla nebo řetězce) je *, druh generických typů (např. seznamu List⟨_⟩) je * \rightarrow * a druh monád je (* \rightarrow *) \rightarrow *. V případě monád jde o druh vyššího řádu.

Konkrétní typy (druhu *) tvoří kategorii, ve které morfismy jsou funkce. Typem druhu * \rightarrow * je v C++ například

template class A;

Typem druhu * \rightarrow * \rightarrow * je například

template class A;

Typem vyššího druhu (* \rightarrow *) \rightarrow * je kupříkladu:

template class T> class A;

Ve většině běžných imperativních jazyků (Java, Swift, Go…) není možné typy vyšších druhů používat kvůli chybějící podpoře v překladači a runtimu. V dynamicky typovaných jazycích (Python, Objective-C apod. +more) je implementace bezproblémová, ovšem bez typové kontroly během překladu.

Kombinátor pevného bodu

Příkladem funkce s typem vyššího druhu je kombinátor pevného bodu, jehož druh je ((* \rightarrow *) \rightarrow * \rightarrow *) \rightarrow * \rightarrow *. V Haskellu se definuje takto:

fix f = let x = f x in x

neboli

fix f = f (fix f)

Kategorie:Teorie typů