Funktsionaalprogrammeerimine 2022/23 sügis

Kodutöö 12

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

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 1 : implementeeri writeAll

Funktsioonikutse writeAll a xs n kirjutab listi xs elemendid massiivi a alustades indeksist n.

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 2: massiivi teisendamine listiks

Funktsioonikutse toLst a i j tagastab massiivi a elemendid indeksitega i kuni j listina.

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 3: 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 4: 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]

Ülesanne 5: Tüübituletus

"Joonista" tüübituletuspuu, kirjuta välja kõik kitsendused ja lahenda kogu avaldise tüüp ɣ2.

Lihtsustuseks:

• ei pea kirjutama xᵅ ∈ Γ
• kitsendusi ei pea kirjutama puu sisse (mis oli slaididel roheline)

Ülesanded:

1. ⊢ (λxᵅ¹. ((λyᵅ². yᵅ³)ˠ¹ xᵅ⁴)ᵝ¹)ˠ²
2. ⊢ (λxᵅ¹. (xᵅ² (λyᵅ³. yᵅ⁴)ˠ¹)ᵝ¹)ˠ²
3. ⊢ (λxᵅ¹. ((λyᵅ². (λzᵅ³. yᵅ⁴)ˠ¹)ˠ³ xᵅ⁵)ᵝ¹)ˠ²
4. ⊢ (λxᵅ¹. ((λyᵅ². (λzᵅ³. zᵅ⁴)ˠ¹)ˠ³ xᵅ⁵)ᵝ¹)ˠ²