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
Esimene argument (tüüp a) on loogeliste sulgude vahel, mis tähendab et see on implitsiitne ehk tuletatav. See tähendab, et väljakutsel ei pea seda argumenti andma ja idris püüab selle väärtuse ise tuletada.
Käesoleval juhul on tüübiks teise (esimese eksplitsiitse) argumendi tüüp. Selle tüübi saab ka ise anda, näiteks id {a=Int} 5 või id {a=Bool} True .
Väljakutse süntaks tuleneb sellest, et implitsiidseid argumente võib olla järjest mitu ja on vaja teada, millised anda eksplitiitselt ja millised implitsiitselt.
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 [] = []
revVec (x :: ys) = idVec ((revVec ys) `concatVec` [x])
Esiteks, idVec juures teeme mustrisobitust implitiitse argumendi n põhjal. Siin ei ole muud head võimalust, kuna Vec (n + 1) a kuju järgi n-i tuletamine oleks parajalt keeruline. Lisaks pole meil mingit põhjust, miks peaks hoiduma implitiitse argumendi üle mustrisobitust tegemast. Implitiitseid argumente kasutatakse selleks, et funktsioonikutsel ei pea neid kirjutama -- neid saab tuletada teiste argumentide kaudu.
Teiseks, ilma idVec-ta tuleb veateade revVec-s. Idris ei tea, et k + (1 + 0) on S k ehk 1+k.