Kodutöö 11
Sõltuvate tüüpidega programmeerimine
Selles praktikumis harjutame sõltuvate tüüpidega programmeerist.
Konspekt (Sõltuvad tüübid)
Lisalugemine (vabatahtlik):
Type-Driven development with Idris peatükid:
- Chapter 3. Interactive development with types, alampeatükk:
- 3.4. Implicit arguments: type-level variables
Mitmedimensioonilised punktid
Olles loengus tutvunud tüüpide arvutamise kontseptsiooniga, saab defineerida näiteks kahedimensioonilise punkti tüübi:
punkt2d : Type punkt2d = (Double, Double)
ning seda üldistades defineerida funktsiooni, mis arvutab sõltuvalt naturaalarvulisest sisendist sellemõõtmelisse dimensiooni kuuluva punkti tüübi:
punkt : Nat -> Type punkt Z = Unit punkt (S Z) = Double punkt (S n) = (Double, punkt n)
Näiteks:
xy : punkt 2 xy = (2.0,4.0) xyz : punkt 3 xyz = (3.0,6.0,3.0)
Ülesanne 1 - nullpunkt
Erinevate dimensioonide nullpunktide arvutamine. Kirjuta funktsioon, mis arvutab vastavalt naturaalarvulisele sisendile sellelemõõtmelise dimensiooni nullpunkti:
nullpunkt : (d : Nat) -> punkt d nullpunkt d = ?undefined
Näiteks:
nullpunkt 0 == () nullpunkt 1 == 0.0 nullpunkt 2 == (0.0, 0.0)
Ülesanne 2 - add -- liida kahe punkti vastavad koordinaadid
add: (d:Nat) -> punkt d -> punkt d -> punkt d add d x y = ?add_rhs
Näiteks:
add 0 () () == () add 1 1.0 2.0 == 3.0 add 3 (0.2, 0.2, 4.0) (1.0, 2.0, 0.2) == (1.2, 2.2, 4.2)
Ülesanne 3 - sum - liida kõigi listis olevate punktide koordinaadid
Kirjuta funktsioon, mis võtab sisse naturaalarvu ja sellele vastavasse dimensiooni kuuluvate punktide listi ning tagastab punkti, mille koordinaatideks on teise argumendina saadud listis olevate punktide vastavate koordinaatide summa, kasutades selleks eeldefineeritud funktsioone nullpunkt ja add:
sum : (d : Nat) -> List (punkt d) -> punkt d sum d xs = ?sum_rhs
Näiteks:
sum 0 [] == () sum 2 [(1.0,1.0), (2.0,2.0)] == (3.0, 3.0)
Vektorid
Kõige klassikalisem näide Idrise sõltuvatest tüüpidest on vektorid. Vektorid on listid, mis on parametriseeritud nende pikkuse suhtes. See tähendab, et lisaks listile endale sisaldub tüübis alati ka selle pikkus.
data Vect : (k : Nat) -> (a : Type) -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
Eq a => Eq (Vect k a) where
[] == [] = True
(x :: y) == (z :: w) = x==z && y==w
Väärtuse tüüp on staatiline (ehk kompileerimisaegne) info selle väärtuse kohta. Tüübi täpsustamisega liigutame osa dünaamilist infot staatiliseks. S.t., kui mingis programmis on listide pikkused teada (või väga selge loogikaga), siis on mõistlik kasutada vektoreid. Või siis vastupidi: kui listi pikkust pole teada, siis pole selles kohas mõtet vektoreid kasutada.
Kahe vektori konkateneerimise funktsioon on seega defineeritud kui
append : Vect n a -> Vect m a -> Vect (n + m) a append [] ys = ys append (x :: xs) ys = x :: append xs ys
Ülesanne 4 - zipVect
zipVect : Vect n a -> Vect n b -> Vect n (a,b) zipVect = ?zipVect_rhs
Näiteks:
zipVect [1,2,3] ['a', 'b', 'c'] == [(1, 'a'), (2, 'b'), (3, 'c')]
Ülesanne 5 - replaceVect
Asendamine vektorites.
replaceVect : a -> (n:Nat) -> Vect (1+n+k) a -> Vect (1+n+k) a replaceVect = ?replaceVect_rhs
Näiteks:
replaceVect 'x' 0 ['a','b','c','d'] == ['x', 'b', 'c', 'd'] replaceVect 'x' 1 ['a','b','c','d'] == ['a', 'x', 'c', 'd'] replaceVect 'x' 2 ['a','b','c','d'] == ['a', 'b', 'x', 'd']
Ülesanne 6 - takeVec
alguse võtmine vektoritest
min : Nat -> Nat -> Nat
min 0 y = 0
min (S k) 0 = 0
min (S k) (S j) = S (min k j)
takeVec : (n:Nat) -> {m:Nat} -> Vect m a -> Vect (min n m) a
takeVec n {m} xs = ?takeVec1
Pane tähele, et takeVec teine argument 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 võetakse selle argumendi väärtus vektori argumendist. Samas, selle argumendi saab ka "käsitsi" anda, näiteks takeVec 3 {m=5} [1,2,3,4,5]. (Süntaks tuleneb sellest, et implitsiidseid argumente võib olla järjest mitu ja on vaja teada, millised anda eksplitiitselt ja millised implitsiitselt.)
Näiteks:
takeVec 4 [1,2,3,4,5,6,7] == [1, 2, 3, 4]
takeVec 0 [1,2,3,4,5,6,7] == []
takeVec 100 [1,2,3,4,5,6,7] == [1, 2, 3, 4, 5, 6, 7]
takeVec 100 {m=7} [1,2,3,4,5,6,7] == [1, 2, 3, 4, 5, 6, 7]
Sõltuvate tüüpidega programmeerimine -- kujulised puud
Listi pikkust saab käsitleda ka kui selle kuju. Andmestruktuuri kujuks on andmestruktuuri tekitatav vari:
[] [1] [1,2] [1,2,3] [] [▒] [▒,▒] [▒,▒,▒] Z S Z S S Z S S S Z
Listi kujuks on selle pikkus, milleks on naturaalarv. Sarnase mõttekäiguga saab luua ka sõltuva tüübiga puud, mille tüüp sõltub puu kujust.
Kui jääte (kodus) hätta, siis vektorite ja kujuliste puude kohta väga hea loengu leiate TalTech-i FP kursuselt, siit.
data TreeShape : Type where
LeafShape : TreeShape
NodeShape : (l : TreeShape) -> (r : TreeShape) -> TreeShape
data Tree : TreeShape -> Type -> Type where
Leaf : Tree LeafShape a
Node : (left : Tree l a) -> (this : a) -> (right : Tree r a) ->
Tree (NodeShape l r) a
Eq TreeShape where
LeafShape == LeafShape = True
LeafShape == (NodeShape l r) = False
(NodeShape l r) == LeafShape = False
(NodeShape l r) == (NodeShape x y) =
l==x && r==y
Eq a => Eq (Tree s a) where
Leaf == Leaf = True
(Node left this right) == (Node x y z) =
left == x && this == y && right == z
tr1 : Tree (NodeShape LeafShape (NodeShape LeafShape LeafShape)) Int
tr1 = Node Leaf 1 (Node Leaf 2 Leaf)
tr2 : Tree (NodeShape LeafShape (NodeShape LeafShape LeafShape)) Int
tr2 = Node Leaf 3 (Node Leaf 1 Leaf)
Ülesanne 7 - zip_tree
Zip tavaliste puude puhul:
-- data Tree : Type -> Type where -- Leaf : Tree a -- Node : Tree a -> a -> Tree a -> Tree a -- -- zip_tree : Tree a -> Tree b -> Tree (a, b) -- zip_tree Leaf Leaf = Leaf -- zip_tree Leaf (Node left this right) = Leaf -- zip_tree (Node left this right) Leaf = Leaf -- zip_tree (Node left1 this1 right1) (Node left2 this2 right2) = -- Node (zip_tree left1 left2) (this1 , this2) (zip_tree right1 right2)
Nüüd tehke sama kujuliste puudega:
zip_tree : Tree shape a -> Tree shape b -> Tree shape (a, b) zip_tree x y = ?zip_tree_rhs
Näide:
zip_tree tr1 tr1 == Node Leaf (1, 1) (Node Leaf (2, 2) Leaf) zip_tree tr1 tr2 == Node Leaf (1, 3) (Node Leaf (2, 1) Leaf)
Ülesanne 8 - flip_tree
Implementeerige kujuliste puude ümberpööramine
flip_shape : TreeShape -> TreeShape flip_shape LeafShape = LeafShape flip_shape (NodeShape l r) = (NodeShape (flip_shape r) (flip_shape l)) flip_tree : Tree shape a -> Tree (flip_shape shape) a flip_tree = ?flipTree_rhs
Näide:
flip_tree tr1 == Node (Node Leaf 2 Leaf) 1 Leaf flip_tree tr2 == Node (Node Leaf 1 Leaf) 3 Leaf
Ülesanne 9* -- asendamine puudes
Esmalt defineerime tüübi PathTo, millega viidata puude elementidele.
PathTo esimene argument on viidatava elemendi kuju; teine argument on kogu puu kuju.
data PathTo:(targetS:TreeShape) -> (treeS : TreeShape) -> Type where
Here : PathTo targetS targetS
Left : (path : PathTo targetS l) -> PathTo targetS (NodeShape l r)
Right : (path : PathTo targetS r) -> PathTo targetS (NodeShape l r)
Implementeerige puu sees asendamine.
replace_node : a -> PathTo (NodeShape l r) sh -> Tree sh a -> Tree sh a replace_node new path tree = ?replace_node_rhs
Näide:
replace_node 9 (Right Here) tr1 == Node Leaf 1 (Node Leaf 9 Leaf) replace_node 9 Here tr1 == Node Leaf 9 (Node Leaf 2 Leaf)
Ülesanne 10* -- tree concatenation
Puude kujude konkateneerimine: viidatud lehe asemel pannakse esimese argumendi kuju.
shape_graft : (branchS : TreeShape) -> (stalkS : TreeShape) ->
(path : PathTo LeafShape stalkS) -> TreeShape
shape_graft branchS LeafShape Here = branchS
shape_graft branchS (NodeShape l r) (Left path) =
NodeShape (shape_graft branchS l path) r
shape_graft branchS (NodeShape l r) (Right path) =
NodeShape l (shape_graft branchS r path)
Puude konkateneerimine: viidatud lehe asemel pannakse funkstiooni esimene argument.
tree_graft : (branch : Tree branchS a) -> (stalk : Tree stalkS a) ->
(path : PathTo LeafShape stalkS) ->
Tree (shape_graft branchS stalkS path) a
tree_graft branch stalk path = ?tree_graft_rhs
Näide:
tree_graft tr2 tr1 (Left Here) == Node (Node Leaf 3 (Node Leaf 1 Leaf)) 1 (Node Leaf 2 Leaf) tree_graft tr2 tr1 (Right (Right Here)) == Node Leaf 1 (Node Leaf 2 (Node Leaf 3 (Node Leaf 1 Leaf)))