Závislostní typ

Šablona:Neověřeno 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 𝒰$ 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 $𝒰$). Je-li $B$ konstantní, odpovídají součinové typy funkčním typům ($\prod _{(a:A)}B\equiv A\to 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 $\mathrm{Not}(T)\equiv T\supset \mathrm{\perp }$. Dokazatelnost se v teorii typů řídí intuicionistickou logikou, proto zde neplatí zákon o vyloučení třetího.