Cesko.wiki Závislostní typ
Author
Albert FloresZávislostní typ je v teorii typů typ závisející na konkrétní hodnotě. Obecně se rozlišuje mezi závislostními typy součinovými a součtovými.
Je-li A \in \mathcal{U} nějaký typ z univerza typů, pak \prod_{(a:A)}B(a) je součinový závislostní typ, přičemž B je typ závisející na hodnotě a:A. Naopak \sum_{(a:A)}B(a) je součtový závislostní typ. +more Na B lze nahlížet jako na funkci přiřazující hodnotám (typu A) typy (z \mathcal{U}). Je-li B konstantní, odpovídají součinové typy funkčním typům (\prod_{(a:A)}B \equiv A \rightarrow B) a součtové typy kartézskému součinu (\sum_{(a:A)}B \equiv A \times B).
Závislostní typy byly zavedeny do teorie typů za účelem rozšíření Curry-Howardova isomorfismu z logiky výrokové na predikátovou, odpovídají totiž kvantifikátorům logiky prvního řádu. Používají se v některých programovacích jazycích pro silnou typovou kontrolu, zejména v kritických aplikacích, kde je kladen velký důraz na bezpečnost a korektnost programu.
V jazycích se závislostními typy je možné používat funkce v signaturách funkcí, například v jazyce Idris:
getType : Bool -> Type getType True = String getType False = Nat
getValue : (b : Bool) -> getType b getValue True = "abcd" getValue False = 1234
Rovnostní typy a negace
Rovnost dvou objektů lze vyjádřit typem a=_A b. Tento typ má nejvýše jeden konstruktor (právě jeden, pokud a=b), který se značí Refl.
Negace typu je operátor \operatorname{Not}(T) \equiv T \supset\bot. Dokazatelnost se v teorii typů řídí intuicionistickou logikou, proto zde neplatí zákon o vyloučení třetího.