Funktsionaalprogrammeerimine 2021/22 sügis

12. Praktikum

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

Etteantud kood loengust: lineaarne massiiv

import Data.IOArray
import Data.List
import Control.App
import Control.App.Console
import System.Random


%hide Builtin.(#)
%hide Builtin.DPair.(#)

infix 5 #
infix 6 ##

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

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

    -- Sama, mis L aga mõlemad komponendid lineaarsed.

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


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

public 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
  frmLst : List Double -> arr
  toLst  : (1 a : arr) -> L () (List Double)
  delArr : (1 a : arr) -> ()
  -- mälu haldamise jaoks on frmLst ebaturvaline, tuleks teha:
  -- withArray : ((1 a : arr) -> L arr c) -> c   


--loengust
mapArr : Array arr => (Double -> Double) -> (1 _ : arr) -> arr
mapArr f a = 
    let a # sizea = size a in
    h sizea a
where
    h : Nat -> (1 _ :arr) -> arr
    h Z     a = a
    h (S n) a = let a # v = read a n 
                    a     = write a n (f v) 
                in
                h n a

--loengust
copyAll : Array arr => (1 src : arr) -> (1 dst : arr) -> LL arr arr
copyAll src dst = 
    let src # sizes = size src in
    let dst # sized = size dst in
    if sizes == sized then
        h sizes src dst
    else
        src ## dst
  where
    h : Nat -> (1 _ :arr) -> (1 _ :arr) -> LL arr arr
    h Z     a b = a ## b
    h (S n) a b = let a # va = read a n 
                      b      = write b n va 
                  in
                    h n a b

-- Testimiseks vaja liides implementeerida.
-- Ei pea kõigest aru saama.

data LinArray = MkLinArray (IOArray Double)

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

toListIOArr : IOArray Double -> IO (List Double)
toListIOArr a = 
    let l = Data.IOArray.max a in
    do xs <- traverse (readArray a) [0..l]
       pure (takeWhileJust xs)
  where
    takeWhileJust : List (Maybe b) -> List b
    takeWhileJust (Just x :: xs) = x :: takeWhileJust xs
    takeWhileJust _ = []

int2nat : Int -> Nat 
int2nat x = 
    if x <= 0 then 0 else S (int2nat (x-1))

Array LinArray where
    frmLst xs = MkLinArray $ unsafePerformIO (newIOArr xs)

    toLst (MkLinArray a) = unsafePerformIO (do xs <- toListIOArr a
                                               pure (() # xs)) 

    delArr (MkLinArray a) = ()

    size (MkLinArray a) = MkLinArray a # (int2nat (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))

newLinArr : List Double -> LinArray
newLinArr = frmLst

Ülesanne 1 : implementeeri massiivis elementide vahetamist

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

Ülesanne 2: quickSort-i tsükkel

See on peaaegu standard quick-sort -- ainult natuke mugandatud Nat-idega arvutamiseks, mis ei võimalda negatiivseid indekseid. S.t. võib vaadata algoritmi selgitust siin aga pea meeles, et indeks i algab meil nullist.

pseudokood:

 loop a pivot j hi i = 
   while (j<=hi){
      if (a[j] < pivot) {
          swap a[i] a[j]    
          i++
      }
      j++
   }
   return i

Kirjuta tsükliga pseudokood ümber rekursiooniga ja if-dega lineaarseks Idris2 koodiks.

loop: Array arr => (1 a : arr) -> (pivot:Double) -> (j:Nat) 
                -> (hi:Nat) -> (i:Nat) -> L arr Nat
loop a pivot j hi i = ?loop_rhs

test_loop : (List Double, Nat)
test_loop =
    let 1 a     = newLinArr [0,1,4,5,3]
        a # i   = loop a 3 0 3 0  -- viimane element (pivot): 3 
        () # al = toLst a         -- esimene indeks: 0
    in                            -- eelviimane indeks: 3
    (al,i)                        -- esimene indeks: 0
-- pivot 3 jääb lõppu 
-- listi alguses 3-st väiksemad elemendid
-- listi lõpus (v.a. viimane) 3-st suuremad elemendid
-- i=2 s.t. esimene 3-st suurem element on 2
--
-- Main> :exec printLn test_loop
-- ([0.0, 1.0, 4.0, 5.0, 3.0], 2)

Ülesanne 3: quickSort-i partition

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

Kirjuta pseudokood ümber lineaarseks Idris2 koodiks.

 
-- 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 = ?partition_rhs

test_part : (List Double, Nat)
test_part =
    let 1 a     = newLinArr [0,1,4,5,3]
        a # i   = partition a 0 4   -- esimene indeks: 0
        () # al = toLst a           -- viimane indeks: 4
    in
    (al,i)
-- pivot 3 on indeksil i=2 
-- listi alguses 3-st väiksemad elemendid
-- listi lõpus 3-st suuremad elemendid
--
-- Main> :exec printLn test_part
-- ([0.0, 1.0, 3.0, 5.0, 4.0], 2)

Ülesanne 4: quickSort-i peafunktsioon

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                  

Kirjuta pseudokood ümber lineaarseks Idris2 koodiks.

qs : Array arr => (1 a : arr) -> (lo: Nat) -> (hi: Nat) -> arr
qs a lo hi = ?qs_rhs

-- sorteerib kogu massiivi
quickSort : Array arr => (1 _ : arr) -> arr
quickSort a = 
    let a # len = size a in
    qs a 0 (decr len)

test_qs : List Double
test_qs =
    let 1 a = newLinArr [5,4,7,6,1,2]
        a   = quickSort a
        () # al = toLst a
    in
    al
-- Main> :exec printLn test_qs
-- [1.0, 2.0, 4.0, 5.0, 6.0, 7.0]

Nüüd vaatame IO-d läbi lineaarsete tüüpide

Sarnaselt massiividele ei taha me alles hoida (arvuti) eelnevaid seisundeid.

public export
interface MyHasIO world where
  writeConsole  : (1 _ : world) -> String -> world
  readConsole   : (1 _ : world) -> L world String
  rnd           : (1 _ : world) -> Int -> Int -> L world Int

--- implementatsioon (pole tähtis)

private
data World : Type where
    MkWorld : World

MyHasIO World where
    writeConsole MkWorld xs = unsafePerformIO (do putStrLn xs
                                                  pure MkWorld)
    readConsole MkWorld = unsafePerformIO (do l <- getLine
                                              pure (MkWorld # l))
    rnd MkWorld l h =  unsafePerformIO (do l <- randomRIO (l,h)
                                           pure (MkWorld # l))

runIO : Show b => ((1 _ : World) -> L World b) -> IO b
runIO prg = 
    let MkWorld # y = prg MkWorld in
    pure y

Ülesanne 5: io-ga programm

  rnd           : (1 _ : world) -> Int32 -> Int32 -> L world Int32

1. lugeda konsoolist rida s
2. genereerida juhuarv i <- [2..6]
3. txt = concat (replicate (cast i) s)
4. trükkida välja txt ehk i korda sisestatud tekst s

prog1 : MyHasIO world => (1 w : world) -> L world ()
prog1 w = ?prog1_rhs
-- Main> :exec runIO prog1
-- tere
-- tereteretere

Ülesanne 6: massiivi kõigi elementide trükkimine

Vaata testi ja täida lüngad!

printArray: (MyHasIO wrld, Array arr)=> (1 a: arr) -> (1 w: wrld) -> LL wrld arr
printArray a w =  
    let a # l  = size a 
        w ## a = printElem w a l 
    in w ## a
        where printElem : (1 w: wrld) -> (1 a: arr) -> Nat -> LL wrld arr
              printElem w a n = ?printElem_rhs

testPrint : MyHasIO wrld =>  (1 w: wrld) -> L wrld ()
testPrint w = 
    let 1 a    = newLinArr [1,2,3,4]
        w ## a = printArray a w
        ()     = delArr a
    in w # ()

-- Main> :exec runIO testPrint
-- 1.0
-- 2.0
-- 3.0
-- 4.0

Ülesanne 7: massiivi elementide ülekirjutamine käsurealt

fillArray loeb käsurealt järjest sõnesid v ja kirjutab (cast v) masiivi. Vaata testi ja täida lüngad!

fillArray: (MyHasIO wrld, Array arr)=> (1 a: arr) -> (1 w: wrld) -> 
    (lo:Nat) -> (hi:Nat) -> LL wrld arr
fillArray a w lo hi = ?fillArray_rhs

testFill : MyHasIO wrld =>  (1 w: wrld) -> L wrld ()
testFill w = 
    let 1 a    = newLinArr [1,2,3,4]
        w ## a = fillArray a w 0 3
        w      = writeConsole w "------"
        w ## a = printArray a w
        ()     = delArr a
    in w # ()
-- Main> :exec runIO testFill
-- 5
-- 6
-- 7
-- 8
-- ------
-- 5
-- 6
-- 7
-- 8

Ülesanne 8: käsurealt sorteerija

Implementeeri testSort nii, et loetakse käsurealt neli arvu ja trükitakse need sorteeritult konsooli. (kasutada quickSort-i)

testSort :  MyHasIO wrld =>  (1 w: wrld) -> L wrld ()
testSort w = ?testSort_rhs

-- Main>:exec runIO testSort
-- 6
-- 8
-- 3
-- 2
-- ------
-- 2
-- 3
-- 6
-- 8