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

module K14

import Data.IOArray
import Data.List
import System.Random

%hide Builtin.infixr.(#)
%hide Builtin.DPair.(#)
%hide Builtin.swap
%hide Data.List.partition

infix 7 #

data L : Type -> Type -> Type where
    (#) : (1 _ : a) -> b -> L a b

    -- Konstrueerimine: lineaarset resrurssi saab panna esimeseks 
    -- komponendiks, aga siis on terve paar lineaarne.

    -- Mustrisobitusel: kui kogu paar peab olema lineaarne, siis
    -- selle esimene komponent on lineaarne.

(Show a, Show b) => Show (L a b) where
    show (x # y) = show x ++ " # " ++ show y

(Eq a, Eq b) => Eq (L a b) where
    (x#y) == (z#w) = x==z && y==w

-- Lihtsustus: Double-te massiivid (indekseeritud Int-dega) 

export
interface Array arr where
    write  : (1 a : arr) -> Int -> Double -> arr
    read   : (1 a : arr) -> Int -> L arr Double
    size   : (1 a : arr) -> L arr Int
    withArray : Int -> ((1 a : arr) -> L arr c) -> c     


export
Array (List Double, Int) where
    write (xs, n) i y = (writeList xs i y, n)
        where writeList : List Double -> Int -> Double -> List Double
              writeList [] k y = replicate (cast k) 0 ++ [y]
              writeList (_ :: xs) 0  y = y :: xs
              writeList (x :: xs) k y = x :: writeList xs (k-1) y

    read (x, n) i = (x, n) # readList x i
        where readList : List Double -> Int -> Double
              readList [] k = 0
              readList (x ::  _) 0 = x 
              readList (_ :: xs) k = readList xs (k-1)

    size (xs, n) = (xs, n) # n

    withArray n f = 
        let _ # x = f ([], n) in x

export
data LinArray = MkLinArray (IOArray Double)


export
Array (LinArray, Int) where
    withArray n f =
        unsafePerformIO (do a <- newArray (cast n)
                            let (_ # r) = f (MkLinArray a, n)
                            pure r )

    size (MkLinArray a, n) = (MkLinArray a, n) # n

    write (MkLinArray a, n) i v =
        unsafePerformIO (do ok <- writeArray a (cast i) v
                            pure (MkLinArray a, n))
    read (MkLinArray a, n) i =
        unsafePerformIO (do r <- readArray a (cast i)
                            case r of
                                Just v  => pure ((MkLinArray a, n) # v)
                                Nothing => pure ((MkLinArray a, n) # 0))

withLinArray : Int -> ((1 _ : (LinArray, Int)) -> L (LinArray, Int) c) -> c
withLinArray = withArray

withListArray : Int -> ((1 _ : (List Double, Int)) -> L (List Double, Int) c) -> c
withListArray = withArray


toList : Array arr => (1 src: arr) -> L arr (List Double)
toList a = 
    let a # n = size a in 
    h (n-1) a []


        where h : Int -> (1 src: arr) -> List Double -> L arr (List Double)
              h j a acc =
                if j<0 then a # acc else
                let a # x = read a j in
                h (j-1) a (x::acc)

copyList : Array arr => List Double -> (1 src: arr) -> arr 
copyList xs a = h 0 xs a

        where h : Int -> List Double -> (1 src : arr) -> arr
              h i [] a = a
              h i (x :: xs) a = h (i+1) xs (write a i x)

minDouble : Double
minDouble = -1.7976931348623157e+308

maxDouble : Double
maxDouble = 1.7976931348623157e+308

test : (List Double, Int)
test = ([10.0,11.0,12.0,13.0,14.0],5)

Pane tähele, et massiivide jaoks on antud kaks definitsiooni. Testimiseks listid ja reaalsema näitena IO-massiivid.

Ülesanne 1: implementeeri massiivis elementide vahetamine

Lineaarne funktsioon vahetab massiivis vastavad indeksid ja tagastab massiivi.

 
swap : Array arr => Int -> Int -> (1 _ : arr) -> arr
swap i j a = ?swap_rhs

test:

 K14> K14.swap 2 4 test
 ([10.0, 11.0, 14.0, 13.0, 12.0], 5)
 K14> K14.swap 0 4 test
 ([14.0, 11.0, 12.0, 13.0, 10.0], 5)

Ülesanne 2: implementeeri massiivi elementide summeerimine

Lineaarne funktsioon sumArray n a liidab massiivis a elemendid indeksitega 0 kuni n (kaasa arvatud). Lahenda lihtrekursiooniga, et igal rekursiivsel kutsel n väheneb ühe võrra.

 
sumArray : Array arr => Int -> (1 _ : arr) -> L arr Double
sumArray n a = ?sumArray_rhs

test:

 K14> sumArray 0 test
 ([10.0, 11.0, 12.0, 13.0, 14.0], 5) # 10.0
 K14> sumArray (-1) test
 ([10.0, 11.0, 12.0, 13.0, 14.0], 5) # 0.0
 K14> sumArray 4 test
 ([10.0, 11.0, 12.0, 13.0, 14.0], 5) # 60.0

Testi summeerimist ka päris massiividel

 
withLinTestArray :  (((1 _ : (LinArray, Int)) -> L (LinArray, Int) c)) -> c
withLinTestArray f = 
    withLinArray (snd test) (\a => f (copyList (fst test) a))

Test:

 K14> :exec printLn (withLinTestArray (sumArray 0))
 10.0
 K14> :exec printLn (withLinTestArray (sumArray 4))
 60.0

Ülesanne 3: implementeeri massiivi ümberpööramine

Lineaarne funktsioon rev a tagastab massiivi, mille elemendid on esialgsega võrreldes vastupidises järjekorras.

 
rev : Array arr => (1 _ : arr) -> arr
rev a = 
    let a # n = size a in
    f 0 (n-1) a
     where f : Int -> Int -> (1 _ : arr) -> arr
           f i j a = ?f_rhs

test:

 K14> rev test
 ([14.0, 13.0, 12.0, 11.0, 10.0], 5)

Testi ümberpöötamist ka päris massiividel

 
withLinTestArray' :  (((1 _ : (LinArray, Int)) -> (LinArray, Int))) -> List Double
withLinTestArray' f = 
    withLinArray (snd test) (\a => toList (f (copyList (fst test) a)))

test:

 K14> :exec printLn (withLinTestArray' rev)
 [14.0, 13.0, 12.0, 11.0, 10.0]

Ülesanne 4: implementeeri massiivi map operatsioon

Lineaarne funktsioon map f a tagastab massiivi, mille elemendidele on rakendatud funktsioon f.

 
mapArray : Array arr => (Double -> Double) -> (1 _ : arr) -> arr
mapArray f a = 
    let a # n = size a in
    g (n-1) a
    where g : Int -> (1 _ : arr) -> arr
          g n a = ?g_rhs

test:

 K14> mapArray (+100) test
 ([110.0, 111.0, 112.0, 113.0, 114.0], 5)

Ülesanne 5: implementeeri massiivi fold operatsioon

 
foldArray : Array arr => (acc -> Double -> acc) -> acc -> (1 _ : arr) -> L arr acc
foldArray f x a = 
    let a # n = size a in
    h (n-1) a
    where h : Int -> (1 _ : arr) -> L arr acc
          h n a = ?h_rhs

test:

 K14> foldArray max minDouble test
 ([10.0, 11.0, 12.0, 13.0, 14.0], 5) # 14.0
 K14> foldArray min maxDouble test
 ([10.0, 11.0, 12.0, 13.0, 14.0], 5) # 10.0
 K14> :exec printLn (withLinTestArray (foldArray min maxDouble))
 10.0

Ülesanne 6: implementeeri massiivi normaliseerimine

Normaliseerimise all mõtleme siin operatsiooni, mis leiab massiivi vähima elemendi v, maksimaalse elemendi s. Operatsioon lahutab kõigist teistest elementidest v ja jagab tulemuse s-v-ga. Seega on tulemuses tavajuhul vähima elemendi indeksil salvestatud null ja maksimaalse elemendi juures 1. Kõik teised elemendid on positiivsed ja vahemikus 0 kuni 1. Lisaks tagastada ka v ja s.

 
normalize : Array arr => (1 _ : arr) -> L arr (Double,Double) 
normalize a = ?normalize_rhs

test:

 K14> normalize test
 ([0.0, 0.25, 0.5, 0.75, 1.0], 5) # (10.0, 14.0)