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:
- ⊢ (λxᵅ¹. ((λyᵅ². yᵅ³)ˠ¹ xᵅ⁴)ᵝ¹)ˠ²
- ⊢ (λxᵅ¹. (xᵅ² (λyᵅ³. yᵅ⁴)ˠ¹)ᵝ¹)ˠ²
- ⊢ (λxᵅ¹. ((λyᵅ². (λzᵅ³. yᵅ⁴)ˠ¹)ˠ³ xᵅ⁵)ᵝ¹)ˠ²
- ⊢ (λxᵅ¹. ((λyᵅ². (λzᵅ³. zᵅ⁴)ˠ¹)ˠ³ xᵅ⁵)ᵝ¹)ˠ²