Vaje

Vaje#

Naloga 1#

Izpeljite in rešite enačbe za izpeljavo tipov naslednjih programov:

|- (fun x -> x * x) 14
f : α, v : bool |- if f v then 1 else 0
g : bool -> α |- (fun f -> f (g true)) (fun x -> x + 2)

Preverite, ali vrstni red enačb vpliva na rezultat. Ugotovite kje se pojavi problem pri določanju tipa funkcije fun f -> f f.

Naloga 2#

Algoritem za izpeljavo tipov dopolnite za: rekurzijo, pare, vsote in sezname.

Kot pri dodajanju novih pravil za tipe moramo za vsak nov sintaktični konstrukt dodati pravilo za izpeljavo tipa in dodatne enačbe. Glede na dodajanje novih enačb moramo tudi posodobiti pravila za reševanje sistema enačb.

\begin{array}{r} \begin{matrix} \frac{Γ, f : α \to β, x : α ⊢ M : B ∣ E}{Γ ⊢ rec f x . M : α \to β ∣ α = A, β = B, E} \\ \frac{Γ ⊢ M_{1} : A_{1} ∣ E_{q} Γ ⊢ M_{2} : A_{2} ∣ E_{2}}{Γ ⊢ (M_{1}, M_{2}) : α_{1} \times α_{2} ∣ α_{1} = A_{1}, α_{2} = A_{2}, E_{1}, E_{2}} \\ \frac{Γ ⊢ M : A ∣ E}{Γ ⊢ fst M : α_{1} ∣ α_{1} \times α_{2} = A, E} \\ \frac{Γ ⊢ M : A ∣ E}{Γ ⊢ fst M : α_{2} ∣ α_{1} \times α_{2} = A, E} \\ \frac{Γ ⊢ M : A_{1} ∣ E}{Γ ⊢ inl M : α ∣ α = A_{1} + α_{2}, E} \\ \frac{Γ ⊢ M : A_{2} ∣ E}{Γ ⊢ inr M : α ∣ α = α_{1} + A_{2}, E} \\ \frac{Γ ⊢ M : A ∣ E Γ, x_{1} : α_{1} ⊢ M_{1} : B_{1} ∣ E_{1} Γ, x_{2} : α_{2} ⊢ M_{2} : B_{2} ∣ E_{2}}{Γ ⊢ match M with inl x_{1} \mapsto M_{1} inr x_{2} \mapsto M_{2} : β ∣ β = B_{1}, β = B_{2}, α_{1} + α_{2} = A, E, E_{1}, E_{2}} \\ \frac{}{Γ ⊢ [] : list α ∣ \emptyset} \\ \frac{Γ ⊢ M_{1} : A_{1} ∣ E_{1} Γ ⊢ M_{2} : A_{2} ∣ E_{2}}{Γ ⊢ M_{1} :: M_{2} : α ∣ α = list A_{1}, α = A_{2}, E_{1}, E_{2}} \\ \frac{Γ ⊢ M : A ∣ E_{1} Γ ⊢ M_{1} : A_{1} ∣ E_{2} Γ, x_{1} : α_{1}, x_{2} : α_{2} ⊢ M_{2} : A_{2} ∣ E_{3}}{Γ ⊢ match M with [] \mapsto M_{1} x_{1} :: x_{2} \mapsto M_{2} : α ∣ α = A_{1}, α = A_{2}, A = list α_{1}, A = α_{2}, E_{1}, E_{2}, E_{3}} \end{matrix} \end{array}

Možnosti za dodajanje pravil je več, pri nekaterih lahko že nekoliko rešimo enačbe, lahko pa sestavimo bolj splošna pravila in reševanje enačb prepustimo algoritmu za reševanje. Vseeno pa je treba biti pozoren, napačno pravilo za konstrukcijo seznama bi namreč bilo

\frac{Γ ⊢ M_{1} : A_{1} ∣ E_{1} Γ ⊢ M_{2} : list A_{2} ∣ E_{2}}{Γ ⊢ M_{1} :: M_{2} : α ∣ α = list A_{1}, α = list A_{2}, E_{1}, E_{2}}

saj bi v primeru konstrukcije seznama 1 :: [] za tip [] dobili $α^{'}$ , ki pa ni oblike $list A$ in tipa ne bi mogli izpeljati.

Dodatna pravila za reševanje enačb so potrebna zato, da lahko razrešimo nove oblike tipov, ki smo jih uvedli.

\begin{array}{r} \begin{matrix} \begin{matrix} \frac{A_{1} = B_{1}, A_{2} = B_{2}, E ↘ σ}{A_{1} \times A_{2} = B_{1} \times B_{2}, E ↘ σ} \end{matrix} \\ \begin{matrix} \frac{A_{1} = B_{1}, A_{2} = B_{2}, E ↘ σ}{A_{1} + A_{2} = B_{1} + B_{2}, E ↘ σ} \end{matrix} \\ \frac{A = B, E ↘ σ}{list A = list B, E ↘ σ} \end{matrix} \end{array}

Posodobiti pa moramo tudi funkcijo $f v$ kot

f v (A_{1} \times A_{2}) = f v (A_{1}) \cup f v (A_{2}) f v (A_{1} + A_{2}) = f v (A_{1}) \cup f v (A_{2}) f v (list A) = f v (A)

Z dodajanjem novih oblik tipov je vedno več enačb “nerešljivih”, saj nimajo ujemajočih oblik.

Naloga 3#

Izpeljite tip funkcije map. Napišite še kakšen program, ki uporablja konstrukte iz naloge 2 in mu določite tip.

Vaje

Contents

Vaje#

Naloga 1#

Naloga 2#

Naloga 3#