Klassikaliselt eristava progamemerimiskeeled (näiteks C, Java, Haskell, etc.) tüüpe ja väärtusi. Näiteks on C keele väärtusel 1 on tüüp int ning väärtusel &abs on tüüpi int (*)(int) (viit funktsioonile, mis saab argumendiks täisarvu ja tagastab täisarvu). Enamasti on kohe aru saada, kas tegemist on tüübi või väärtusega.
Seejärel saame vaadata, kuidas tüübid ja väärtused omavahel seostuvad. Mõnes keeles on väärtusel täpselt üks tüüp, mõnes keeles sobivad väärtusele mitmed tüübid. Tüübiteooria kohaselt väärtus valiidne vaid juhul kui tal on mingi tüüp. Valikulise tüüpimisega keeled, nagu Python, jäävad selles küsimuses eriarvamusele.
Tihti võimaldavad programmeerimiskeeled kirjutada väärtusi, millel on sees mainitud tüüpe, või isegi tüüpe, mille on sees mainitud väärtusi. Nii saame vaadata nelja erinevat sõltuvuse vormi ja uurida, mis selline sõltuvus keele kohta ütleb.
the Int 1 on erinev väärtusest the Double 1. Pane tähele, et siin kasutasime eksplitsiitselt tüüpi väärtuse sees, kuid mõlemas avaldises on 1, mis on ühel korral üht tüüpi ja teisel korral teist.
Kui me juba väärtusi tüüpidele parameetriteks hakkame andma, siis kaob sügavam mõte hoida tüüpide ja väärtuste avaldisi eraldi süntaktiliste klassidena. See on nii ka Idrises. Tüübipositsioonis saame kasutada avaldisi, mille tüüp on Type. Väärtuse positsioonis saame kasutada avaldisi, mille tüüp klapib. Seetõttu saame tüübisünonüüme defineerida kui
| 1Pikkus : Type 2Pikkus = Int |
Keeltes, kus sõltuvaid tüüpe teha ei saa on tavaline, et väärtuse ja tüübid on süntaktiliselt erinevad. Näiteks on Haskellis (moodulie Data.Semigroup) defineeritud tüübipere Sum. Tüübis saab kasutada tüübikonstruktorit Sum :: * -> *, näiteks Sum Int. Aga väärtusena saab kasutada andmekonstruktorid Sum :: a -> Sum a, näiteks Sum 1. Ehk siis Sum-il on erinev tähendus vastavalt kontekstile. Idrises sellis olukorda tekkida ei saa — igal definitsioonil on üks tähendus olenemata, kas seda kasutati tüübipositioonil või väärtuse positsioonil.
Nüüd vaatame sõltuvate tüüpidega programmeerimist näidete põhjal. Esmalt vaatame liste. Idrise listid on sisuliselt defineeritud järgnevalt.
| 1data List : Type -> Type where 2 Nil : List a 3 (::) : a -> List a -> List a |
Üks probleem listidega Idrises on, et pole võimalik teha listist elemendi leidmise funktsiooni tüübiga List a -> a, kuna listil ei pruugi olla esimest elementi. Sarnaselt pole võimalik teha listist n-nda elemendi selekteerimist funktsiooniga Nat -> List a -> a. List ei pruugi sisaldada n-ndat elementi. List võib olla täiesti tühi — siis ei saa isegi valet elementi tagastada.
Üks lahendus on panna listile pikkused külge. Selliseid pikkusega liste nimetatakse Idrises vektoriteks (standardteegi moodulis Data.Vect).
| 1data Vect : Nat -> Type -> Type where 2 Nil : Vect 0 a 3 (::) : a -> Vect n a -> Vect (1+n) a 4 5test5 : Vect 3 Int 6test5 = [1,2,3] |
Vektoritel lihtsalt saab defineerida mittetühja listi esimese elemendi leidmise funktsiooni kui ka selekteerimise üldiselt. Problemaatilised juhud on välistatud tüübi põhjal — vektor peab tüübi järgi olema piisavalt suur.
| 1fst : Vect (1+n) a -> a 2fst (x::_) = x 3 4nth : (n:Nat) -> Vect (1+n+m) a -> a 5nth 0 (x :: xs) = x 6nth (S k) (x :: xs) = nth k xs |
Paljudel juhtudel ongi vektorite definitsioon täpselt samas, mis vastav definitsioon listide jaoks. Ehk, kõik töötab samamoodi aga meil on kasutada ka listi pikkus. Vaata näiteks vektorite konkateneerimise ja map-funktsiooni definitsiooni.
| 1concatVect : Vect n a -> Vect m a -> Vect (n+m) a 2concatVect [] ys = ys 3concatVect (x :: y) ys = x :: concatVect y ys 4 5Functor (Vect n) where 6 map f [] = [] 7 map f (x :: y) = f x :: map f y |
Kui vaatame funktsiooni nth n tüüpi, siis näemegi, et tüüp Vect (1+n+m) a -> a sõltub n-i väärtusest. Praktiliselt seda sõltuvate tüüpidega programmeerimine Idrises tähendabki.
nth 0 : Vect (1+m) a -> a
nth 2 : Vect (3+m) a -> a
Nüüd võime küsida, miks kasutatakse siis liste ja mitte alati vektoreid? Vastus on kaheosaline. Esiteks, paljudel juhtudel ei ole definitsioonid samad — tuleb teha palju lisatööd, et tüübikontrolli läbida. Näiteks vaatame listi ümberpööramist funktsiooniga rev.
| 1rev : {n:Nat} -> Vect n a -> Vect n a 2rev [] = [] 3rev (x::xs) = f ((rev xs) `concatVect` [x]) 4 where f : {m:Nat} -> Vect (m+1) a -> Vect (1+m) a 5 f {m=0} [x] = [x] 6 f {m=S m'} (x::xs) = x :: f xs |
Näeme, et lisaks tavapärasele rekursiivsele kutsele ja lõppu konkateneerimisele tuleb teisendada list Vect (m+1) a listiks Vect (1+m) a.
See pole ainuke (parim?) viis vektori ümberpööramiseks, aga piisav et näidata, miks ei saa kasutada täpselt samasugust funktsiooni nagu listide puhul.
Teiseks põhjuseks, miks vektoreid alati ei kasutata on see, et kasu saame me ainult siis, kui teame listi pikkuse kohta mingit olulist infot. Näiteks, et mitu listi on sama pikkusega. Teisisõnu, kui vektor võib olla suvalise arvu elementidega, siis on ikkagi vaja töödelda kõik juhud, ja võime samahästi kasutada tavalisi liste.
Alternatiivina vektoriterle võib kaaluda ka lihtsalt tõestuste kirjutamist, et mingi arvutusega saadud list on piisava pikkusega.
Seega, kokkuvõtteks, sõltuvad tüübid on tähtis osa Curry-Howard’i vastavuses, kuna võimaldab kirjutada väiteid väärtuste kohta. Praktiliselt võimaldab see lisada andmestruktuuridele kitsendusi seoses teiste programmi muutujatega selliselt, et mingid tingimused on tüübikontrollija poolt verifitseeritud. Samas on tuleb iga programmi puhul kaaluda, kas keerulisema struktuuri kasutuselevõtt aitab kokkuvõttes soovitud programmi kirjutada.