Funktsionaalprogrammeerimine 2024/25 sügis

Kodutöö 14 (vabatahtlik)

Selles praktikumis vaatame 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

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]