Kodutöö 11
Tüübituletus ja sõltuvad tüübid
Selles praktikumis harjutame tüübituletust ning programmeerime sõltuvate tüüpidega.
Tüübituletus
Ülesanne 1
Lihtsustuseks:
- ei pea kirjutama xᵅ ∈ Γ
- kitsendusi ei pea kirjutama puu sisse (mis oli slaididel roheline)
"Joonista" tüübituletuspuu, kirjuta välja kõik kitsendused ja lahenda kogu avaldise tüüp ɣ2 järgnevatele avaldistele:
- ⊢ (λxᵅ¹. ((λyᵅ². yᵅ³)ˠ¹ xᵅ⁴)ᵝ¹)ˠ²
- ⊢ (λxᵅ¹. (xᵅ² (λyᵅ³. yᵅ⁴)ˠ¹)ᵝ¹)ˠ²
- ⊢ (λxᵅ¹. ((λyᵅ². (λzᵅ³. yᵅ⁴)ˠ¹)ˠ³ xᵅ⁵)ᵝ¹)ˠ²
- ⊢ (λxᵅ¹. ((λyᵅ². (λzᵅ³. zᵅ⁴)ˠ¹)ˠ³ xᵅ⁵)ᵝ¹)ˠ²
Sõltuvate tüüpidega programmeerimine
Mitmedimensioonilised punktid
Olles loengus tutvunud tüüpide arvutamise kontseptsiooniga, saab defineerida näiteks kahedimensioonilise punkti tüübi:
1 2 |
punkt2d : Typepunkt2d = (Double, Double) |
ning seda üldistades defineerida funktsiooni, mis arvutab sõltuvalt naturaalarvulisest sisendist sellemõõtmelisse dimensiooni kuuluva punkti tüübi:
1 2 3 4 |
punkt : Nat -> Typepunkt Z = Unitpunkt (S Z) = Doublepunkt (S n) = (Double, punkt n) |
Näiteks:
1 2 3 4 5 |
xy : punkt 2xy = (2.0,4.0)xyz : punkt 3xyz = (3.0,6.0,3.0) |
Ülesanne 2 - nullpunkt
Erinevate dimensioonide nullpunktide arvutamine. Kirjuta funktsioon, mis arvutab vastavalt naturaalarvulisele sisendile sellelemõõtmelise dimensiooni nullpunkti:
1 2 |
nullpunkt : (d : Nat) -> punkt dnullpunkt d = ?undefined |
Näiteks:
nullpunkt 0 == () nullpunkt 1 == 0.0 nullpunkt 2 == (0.0, 0.0)
Ülesanne 3 - add -- liida kahe punkti vastavad koordinaadid
1 2 |
add: (d:Nat) -> punkt d -> punkt d -> punkt dadd d x y = ?add_rhs |
Näiteks:
add 0 () () == () add 1 1.0 2.0 == 3.0 add 3 (0.2, 0.2, 4.0) (1.0, 2.0, 0.2) == (1.2, 2.2, 4.2)
Ülesanne 4 - sum - liida kõigi listis olevate punktide koordinaadid
Kirjuta funktsioon, mis võtab sisse naturaalarvu ja sellele vastavasse dimensiooni kuuluvate punktide listi ning tagastab punkti, mille koordinaatideks on teise argumendina saadud listis olevate punktide vastavate koordinaatide summa, kasutades selleks eeldefineeritud funktsioone nullpunkt ja add:
1 2 |
sum : (d : Nat) -> List (punkt d) -> punkt dsum d xs = ?sum_rhs |
Näiteks:
sum 0 [] == () sum 2 [(1.0,1.0), (2.0,2.0)] == (3.0, 3.0)
Vektorid
Kõige klassikalisem näide Idrise sõltuvatest tüüpidest on vektorid. Vektorid on listid, mis on parametriseeritud nende pikkuse suhtes. See tähendab, et lisaks listile endale sisaldub tüübis alati ka selle pikkus.
1 2 3 4 5 6 7 |
data Vect : (k : Nat) -> (a : Type) -> Type where Nil : Vect Z a (::) : a -> Vect k a -> Vect (S k) aEq a => Eq (Vect k a) where [] == [] = True (x :: y) == (z :: w) = x==z && y==w |
Väärtuse tüüp on staatiline (ehk kompileerimisaegne) info selle väärtuse kohta. Tüübi täpsustamisega liigutame osa dünaamilist infot staatiliseks. S.t., kui mingis programmis on listide pikkused teada (või väga selge loogikaga), siis on mõistlik kasutada vektoreid. Või siis vastupidi: kui listi pikkust pole teada, siis pole selles kohas mõtet vektoreid kasutada.
Kahe vektori konkateneerimise funktsioon on seega defineeritud kui
1 2 3 |
append : Vect n a -> Vect m a -> Vect (n + m) aappend [] ys = ysappend (x :: xs) ys = x :: append xs ys |
Ülesanne 5 - zipVect
1 2 |
zipVect : Vect n a -> Vect n b -> Vect n (a,b)zipVect = ?zipVect_rhs |
Näiteks:
zipVect [1,2,3] ['a', 'b', 'c'] == [(1, 'a'), (2, 'b'), (3, 'c')]
Ülesanne 6 - replaceVect
Asendamine vektorites.
1 2 |
replaceVect : a -> (n:Nat) -> Vect (1+n+k) a -> Vect (1+n+k) areplaceVect = ?replaceVect_rhs |
Näiteks:
replaceVect 'x' 0 ['a','b','c','d'] == ['x', 'b', 'c', 'd'] replaceVect 'x' 1 ['a','b','c','d'] == ['a', 'x', 'c', 'd'] replaceVect 'x' 2 ['a','b','c','d'] == ['a', 'b', 'x', 'd']
Ülesanne 7* - takeVec
alguse võtmine vektoritest
1 2 3 4 5 6 7 |
min : Nat -> Nat -> Nat min 0 y = 0min (S k) 0 = 0min (S k) (S j) = S (min k j)takeVec : (n:Nat) -> {m:Nat} -> Vect m a -> Vect (min n m) atakeVec n {m} xs = ?takeVec1 |
Näiteks:
takeVec 4 [1,2,3,4,5,6,7] == [1, 2, 3, 4] takeVec 0 [1,2,3,4,5,6,7] == [] takeVec 100 [1,2,3,4,5,6,7] == [1, 2, 3, 4, 5, 6, 7]