V obecnosti je vhodné představit si opravdu hodnoty typů jako důkazy příslušných výroků. Názornější je promyslet si reifikovanou verzi EvenReif : Nat -> Bool -> Type.
Mluvíš v jazyce, ve kterém se vůbec nechytám :-(
Pokusím se to vysvětlit nejdřív úplně bez typů, ale než začnu, jen bych si rád ujasnil - Curry-Howardovu korespondenci chápeš? Na tom se dá hezky stavět.
Promiň, vůbec. Pravděpodobně bych se trochu zorientoval, ale já znám jen Haskell, věci v něm, a některé věci spíše intuitivně. Ale mám bujnou fantazii :-)
Aha. To je právě pro pochopení závislostních typů nezbytně nutné. Naštěstí to není žádná raketová věda. Ti dva pánové si všimli, že existuje isomorfismus mezi typy (tak, jak jsou definovány v Churchově teorii typů v rámci λ kalkulu) a formulemi predikátové logiky, přičemž hodnoty typů odpovídají důkazům formulí. Nepravdě odpovídá prázdný typ (bottom type, tj. uninhabited, “neobydlený”), pravdě jednotkový typ (unit type, má jen jednu hodnotu), konjunkci odpovídá dvojice a disjunkci součtový typ. Akorát nejde o “starou dobrou známou” klasickou logiku prvního řádu, ale o logiku intuicionistickou (to je ovšem detail). Závislostní typy používají právě tuto korespondenci k dokazování korektnosti programů, překladač si typ představí jako formuli, kterou se pokusí dokázat, čímž ověří, že program je správně otypovaný (nebo dojde ke sporu, což signalizuje chybu v typech). To nejlepší na tom je, že funkční typ odpovídá implikaci, třeba v případě toho
Even n → Even (S (S n)) se vlastně říká, že když je
n sudé, tak je sudé i
n+2. Závislostní typy pak jen implementují kvantifikátory, jinak bychom byli ve výrokové logice.