Kodutöö 12
Selles praktikumis jätkame sõltuvate tüüpidega ning vaatame ka lineaarsete tüüpidega arvutamist.
Lisalugemine (vabatahtlik):
Idris 2: Quantitative Type Theory in Action peatükid:
- 2: IDRIS 2 AND QUANTITATIVE TYPES
- 3: RESOURCE USAGE PROTOCOLS
Kui jääte (kodus) hätta, siis vektorite ja kujuliste puude kohta väga hea loengu leiate TalTech-i FP kursuselt, siit.
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.
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 1 - 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 2 - 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 3* -- 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 4* -- 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)))
Lineaarsete tüüpidega programmeerimine
Puhta funktsionaalse programmeerimine üks nõrkus on, et vanad väärtused võivad kättesaadavaks jääda. Ning isegi siis, kui vana väärtus ei ole enam kättesaadav, peab automaatne mälukoris esmalt selle fakti tuvastama ja alles siis saab struktuuri mälu vabastada.
Üks lahendus, mis võimaldab vahetulemuste kustutamist mälust, on programmeerimine lineaarsete tüüpidega.
Etteantud kood loengust: lineaarne massiiv
import Data.IOArray
import Data.List
namespace Massiivid
%hide Builtin.(#)
%hide Builtin.DPair.(#)
infix 5 #
public export
data L : Type -> Type -> Type where
(#) : (1 _ : a) -> b -> L a b
export
interface Array arr where
write : (1 a : arr) -> Nat -> Double -> arr
read : (1 a : arr) -> Nat -> L arr Double
size : (1 a : arr) -> L arr Nat
withArray : Nat -> ((1 a : arr) -> L arr c) -> c
export
Array (List Double) where
write [] n d = []
write (x :: xs) 0 d = d :: xs
write (x :: xs) (S k) d = x :: write xs k d
read [] n = [] # 0.0
read (x :: xs) 0 = (x::xs) # x
read (x :: xs) (S n) =
let _ # r = read xs n in
x::xs # r
size [] = [] # 0
size (x :: xs) = (x :: xs) # (length (x :: xs))
withArray l f =
let _ # r = f (replicate l 0.0) in
r
export
data LinArray = MkLinArray (IOArray Double)
private
newIOArr : List Double -> IO (IOArray Double)
newIOArr xs =
let l = cast (length xs) in
do a <- newArray l
let upd = zip [0..l-1] xs
traverse_ (uncurry $ writeArray a) upd
pure a
export
Array LinArray where
withArray n f =
unsafePerformIO (do a <- newArray (cast n)
let (_ # r) = f (MkLinArray a)
pure r )
size (MkLinArray a) = MkLinArray a # (cast (max a))
write (MkLinArray a) i v =
unsafePerformIO (do ok <- writeArray a (cast i) v
pure (MkLinArray a))
read (MkLinArray a) i =
unsafePerformIO (do r <- readArray a (cast i)
case r of
Just v => pure (MkLinArray a # v)
Nothing => pure (MkLinArray a # 0))
Ülesanne 5 : implementeeri writeAll
Funktsioonikutse writeAll a xs n kirjutab listi xs elemendid massiivi a alustades indeksist n.
(Võite ette kujutada, et massiiv a on ülisuur ja me ei taha selle vahetulemusi mälus hoida.)
writeAll : Array arr => (1 _ : arr) -> List Double -> Nat -> arr writeAll a xs n = ?writeAll_rhs
testimine:
Main> writeAll [1.0,2.0,3.0] [5.0,6.0,7.0] 0
[5.0, 6.0, 7.0]
Ülesanne 6: massiivi teisendamine listiks
Funktsioonikutse toLst a i j tagastab massiivi a elemendid indeksitega i kuni j listina.
(Võite ette kujutada, et massiiv a on ülisuur ja me ei taha selle vahetulemusi mälus hoida. Aga vahel tahame mingit lõiku listina vaadelda.)
toLst : Array arr => (1 _ : arr) -> Nat -> Nat -> L arr (List Double) toLst a s f = ?toLst_rhs
test:
Main> toLst [1.0,2.0,3.0] 0 3 [1.0, 2.0, 3.0] # [1.0, 2.0, 3.0]
Ülesanne 7: implementeeri massiivis elementide vahetamist
swap : Array arr => (1 _ : arr) -> Nat -> Nat -> arr swap a i j = ?swap_rhs
test:
Main> swap [1.0,2.0,3.0] 0 2 [3.0, 2.0, 1.0]
Etteantud kood: quickSort
-- pseudokood:
-- loop a pivot j hi i =
-- while (j>=hi){
-- if (a[j] < pivot) {
-- swap a[i] a[j]
-- i++
-- }
-- j++
-- }
-- return i
loop: Array arr => (1 a : arr) -> (pivot:Double) -> (j:Nat)
-> (hi:Nat) -> (i:Nat) -> L arr Nat
loop a pivot j hi i =
if j > hi then a # i else
let a # aj = read a j in
if aj < pivot then
let a = Main.swap a i j in
loop a pivot (j+1) hi (i+1)
else
loop a pivot (j+1) hi i
-- pseudokood:
-- partition a lo hi =
-- pivot = a[hi] // pivot on viimane element
-- i = loop a pivot lo (hi-1) lo // tsükkel, kus viimast elementi ei vaata
-- swap a[i] a[hi] // nüüd vahetame viimase elemendi
-- return i // tagastame pivot-i indeksi
-- abiks Nat-i vähenamine
decr : Nat -> Nat
decr 0 = 0
decr (S n) = n
partition : Array arr => (1 a : arr) -> (lo: Nat) -> (hi: Nat) -> L arr Nat
partition a lo hi =
let a # pivot = read a hi
a # i = loop a pivot lo (decr hi) lo
a = Main.swap a i hi
in a # i
-- pseudokood:
-- qs a lo hi =
-- if (lo<hi) {
-- pivot_index = partition a lo hi
-- qs a lo (pivot_indeks - 1)
-- qs a (pivot_indeks + 1) hi
-- }
-- return a
qs : Array arr => (1 a : arr) -> (lo: Nat) -> (hi: Nat) -> arr
qs a lo hi =
if (lo>=hi) then a else
let a # pi = partition a lo hi
a = qs a lo (decr pi)
a = qs a (1 + pi) hi
in a
-- sorteerib kogu massiivi
quickSortArray : Array arr => (1 _ : arr) -> arr
quickSortArray a =
let a # len = size a in
qs a 0 (decr len)
testimine:
Main> quickSortArray [3.0,2.0,1.0,4.0] [1.0, 2.0, 3.0, 4.0]
Ülesanne 7: listi sorteerimine kasutades LinArray-t
quickSortList : List Double -> List Double
quickSortList xs = withArray len f
where len : Nat
len = length xs
f : (1 _ : LinArray) -> L LinArray (List Double)
f a = ?f_rhs
testList : List Double
testList = map cast $ concat [[20,18..0],[1,3..19]]
testimine:
Main> :exec printLn $ quickSortList [3.0,2.0,1.0,4.0] [1.0, 2.0, 3.0, 4.0] Main> :exec printLn $ quickSortList testList [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0, 12.0, 13.0, 14.0, 15.0, 16.0, 17.0, 18.0, 19.0, 20.0]