Functional Programming 2021/22 fall

10. Praktikum

NB! Mitmed selle praktikumi ülesanded pärinevad TTÜ kursusest Functional Programming.

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

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']

Kujulised puud

Kui jääte (kodus) hätta, siis vektorite ja kujuliste puude kohta väga hea loengu leiate TalTech-i FP kursuselt, siit.

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.

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)

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)

Ülesanne 6 - zip_tree

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 7 - 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 8* -- 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 9* -- 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)))