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:
punkt2d : Type punkt2d = (Double, Double)
ning seda üldistades defineerida funktsiooni, mis arvutab sõltuvalt naturaalarvulisest sisendist sellemõõtmelisse dimensiooni kuuluva punkti tüübi:
punkt : Nat -> Type punkt Z = Unit punkt (S Z) = Double punkt (S n) = (Double, punkt n)
Näiteks:
xy : punkt 2 xy = (2.0,4.0) xyz : punkt 3 xyz = (3.0,6.0,3.0)
Ülesanne 2 - nullpunkt
Erinevate dimensioonide nullpunktide arvutamine. Kirjuta funktsioon, mis arvutab vastavalt naturaalarvulisele sisendile sellelemõõtmelise dimensiooni nullpunkti:
nullpunkt : (d : Nat) -> punkt d nullpunkt d = ?undefined
Näiteks:
nullpunkt 0 == () nullpunkt 1 == 0.0 nullpunkt 2 == (0.0, 0.0)
Ülesanne 3 - add -- liida kahe punkti vastavad koordinaadid
add: (d:Nat) -> punkt d -> punkt d -> punkt d add 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:
sum : (d : Nat) -> List (punkt d) -> punkt d sum 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.
data Vect : (k : Nat) -> (a : Type) -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
Eq 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
append : Vect n a -> Vect m a -> Vect (n + m) a append [] ys = ys append (x :: xs) ys = x :: append xs ys
Ülesanne 5 - zipVect
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.
replaceVect : a -> (n:Nat) -> Vect (1+n+k) a -> Vect (1+n+k) a replaceVect = ?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
min : Nat -> Nat -> Nat
min 0 y = 0
min (S k) 0 = 0
min (S k) (S j) = S (min k j)
takeVec : (n:Nat) -> {m:Nat} -> Vect m a -> Vect (min n m) a
takeVec 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]