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 ${\displaystyle A\in {\mathcal {U}}}$ nějaký typ z univerza typů, pak ${\displaystyle \prod _{(a:A)}B(a)}$ je součinový závislostní typ, přičemž ${\displaystyle B}$ je typ závisející na hodnotě ${\displaystyle a:A}$. Naopak ${\displaystyle \sum _{(a:A)}B(a)}$ je součtový závislostní typ. Na ${\displaystyle B}$ lze nahlížet jako na funkci přiřazující hodnotám (typu ${\displaystyle A}$) typy (z ${\displaystyle {\mathcal {U}}}$). Je-li ${\displaystyle B}$ konstantní, odpovídají součinové typy funkčním typům (${\displaystyle \prod _{(a:A)}B\equiv A\rightarrow B}$) a součtové typy kartézskému součinu (${\displaystyle \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:^[1]

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 ${\displaystyle a=_{A}b}$. Tento typ má nejvýše jeden konstruktor (právě jeden, pokud ${\displaystyle a=b}$), který se značí Refl.

Negace typu je operátor ${\displaystyle \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.

Reference