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 nějaký typ z univerza typů, pak je součinový závislostní typ, přičemž je typ závisející na hodnotě . Naopak je součtový závislostní typ. Na lze nahlížet jako na funkci přiřazující hodnotám (typu ) typy (z ). Je-li konstantní, odpovídají součinové typy funkčním typům () a součtové typy kartézskému součinu ().

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 . Tento typ má nejvýše jeden konstruktor (právě jeden, pokud ), který se značí Refl.

Negace typu je operátor . Dokazatelnost se v teorii typů řídí intuicionistickou logikou, proto zde neplatí zákon o vyloučení třetího.

Reference