Závislostní typ

Zá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. 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.