Sõltuvad tüübid
Tüüpide tüüp on Type, s.t. tüüpe saab anda funktsioonide parameetriteks ja tüüpe saab tagastada.
Näiteks, saame ise teha tüüpe, mis sõltuvad väärtustest.
Arv : Bool -> Type Arv False = List Int -- False: mittedeterministlik Arv True = Int -- True: deterministlik
Kasutamine:
test1 : Arv True -- sama mis Int test1 = 5 test2 : Arv False -- sama mis List Int test2 = [5..10]
Pane tähele, et nii saame teha väga palju tüüpe, mille väärtus on 5. Ehk teistpidi, väärtuse 5 võimalike tüüpide hulk on lõpmatu -- pole võimalik tuletada kõige üldisemat tüüpi.
Saame ise teha tüüpe, mis sõltuvad tüüpidest.
MyList : Type -> Type MyList a = Either () (a,MyList a) list1 : MyList Int list1 = Right (1, Right (2, Right (3, Left ())))
Nägime seda, et funktsiooni tagastus-väärtus sõltub parameetritest, olgu need siis ise tüübid või väärtused.
Funktsioon on n.n. sõltuva tüübiga, kui selle tagastustüüp sõltub funktsiooni parameetrist. Selleks on laiendatud funktsiooni tüübi süntaksit, et saaks funktsiooni tagastus-tüübis viidata parameetri väärtusele.
A -> B -- mittesõltuv funktsioonitüüp (x: A) -> B -- sõltuv funktsioonitüüp, kus x viitab funktsiooni parameetrile (tüübiga A)
plus : (b:Bool) -> Arv b -> Arv b -> Arv b plus True a b = a+b plus False xs ys = [ x+y | x<-xs, y<-ys ]
Main> plus True test1 test1 10
Sõltuva tüübi parameetri tuletamine
Tuletamine on Idrises võimalik.
id : {a:Type} -> a -> a
id x = x
Main> id True
True
Main> id 5
5
Tuletamine pole alati võimalik. Näiteks juhul, kui argumendi tüüp on lihtsustunud Arv True {$\to$} Int. Siis ei suuda Idris võrdusest Arv b == Int tuletada, et b == True.
Sõltuvad andmestruktuurid
Üks viis, et lihtsustamist ei toimuks, on uue andmestruktuuri loomine.
data Arv2 : Bool -> Type where
Det : Int -> Arv2 True
NonDet : List Int -> Arv2 False
test3 : Arv2 True
test3 = Det 5
test4 : Arv2 False
test4 = NonDet [5..10]
Nüüd saame väärtuse järgi tuletada tüübi.
plus2 : Arv2 b -> Arv2 b -> Arv2 b plus2 (Det x) (Det y) = Det (x+y) plus2 (NonDet xs) (NonDet ys) = NonDet [ x+y | x<-xs, y<-ys ]
Main> plusSama3 test3 test3
Det 10
Näide: pikkusega listid (vektorid)
Tavalised listid (uue süntaksi abil)
-- data List : Type -> Type where -- Nil : List a -- (::) : a -> List a -> List a
Paneme pikkused külge:
data Vec : Nat -> Type -> Type where
Nil : Vec 0 a
(::) : a -> Vec n a -> Vec (1+n) a
Näide:
test5 : Vec 3 Int test5 = [1,2,3]
Vektorite konkateneerimine
concatVec : Vec n a -> Vec m a -> Vec (n+m) a concatVec [] ys = ys concatVec (x :: y) ys = x :: concatVec y ys
Vektorite map
Functor (Vec n) where
map f [] = []
map f (x :: y) = f x :: map f y
Ümberpööramine
Listide ümberpööramine:
revList : List a -> List a revList [] = [] revList (x :: ys) = (revList ys) ++ [x]
Vektorite ümberpööramine:
idVec : {n:Nat} -> Vec (n + 1) a -> Vec (1 + n) a
idVec {n = 0} xs = xs
idVec {n = (S k)} (x :: ys) = x :: idVec ys
revVec : {n:Nat} -> Vec n a -> Vec n a
revVec {n=0} [] = []
revVec {n=S k} (x :: ys) = idVec ((revVec ys) `concatVec` [x])
Ilma idVec-ta tuleb veateade. Idris ei tea, et k + (1 + 0) on S k ehk 1+k.