Institute of Computer Science
  1. Courses
  2. 2022/23 fall
  3. Functional Programming (LTAT.03.019)
ET
Log in

Functional Programming 2022/23 fall

  • Üldinfo
    • Õppekorraldus
  • Loeng
    • Baasväärtused ja tüübid
    • 𝜆-arvutus
    • Kõrgemat järku funktsioonid
    • Interaktiivne programmeerimine
    • Uute tüüpide loomine
    • Liidesed
    • Sisend-Väljund
    • Laiskus
    • Lihtsalt tüübitud 𝜆-arvutus
    • Sõltuvad tüübid
    • Tõestamine Idrises
    • Kvantitatiivne tüübiteooria
  • Praktikum
    • KKK
    • Installimine
    • Kodutöö 1
    • Kodutöö 2
    • Kodutöö 3
    • Kodutöö 4
    • Kodutöö 5
    • Kodutöö 6
    • Kodutöö 7
    • Kodutöö 8
    • Kodutöö 9
    • Kodutöö 10
    • Kodutöö 11
    • Kodutöö 12
    • Kordamine
    • Projektid
  • Moodle
  • Zulip (sisselogides näed linki)

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ᵅ⁵)ᵝ¹)ˠ²

 

  • Institute of Computer Science
  • Faculty of Science and Technology
  • University of Tartu
In case of technical problems or questions write to:

Contact the course organizers with the organizational and course content questions.
The proprietary copyrights of educational materials belong to the University of Tartu. The use of educational materials is permitted for the purposes and under the conditions provided for in the copyright law for the free use of a work. When using educational materials, the user is obligated to give credit to the author of the educational materials.
The use of educational materials for other purposes is allowed only with the prior written consent of the University of Tartu.
Terms of use for the Courses environment