Funkcionální programování
Typovaný lambda kalkulus a HindleyMilner·v typový systém
Petr Pudlák
5. °íjna 2011
Petr Pudlák ()
Funkcionální programování
5. °íjna 2011
1/1
Typovaný lambda kalkulus
Osnova
Typovaný lambda kalkulus
Motivace
Chceme se dop°edu dozv¥d¥t n¥co o lambda termu (o programu).
Nap°íklad:
1
Zda jsou zabudované (£i odvozené) funkce pouºity korektn¥.
Nap°íklad, zda neaplikujeme
2
+
na dv¥ funkce.
Jaký bude výsledek programu (pokud program je normalizující)?
Nap°íklad, bude to £íslo, nebo funkce?
3
Je program normalizující? (N¥které typové systémy to dovedou
rozhodnout.)
2/1
Typovaný lambda kalkulus
Typované lambda kalkuly
Krom¥ term· konstruujeme dal²í syntaktické objekty typy.
Denujeme relaci mezi termy a typy: term M je typu
Zna£íme obvykle M
τ .
: τ.
Relaci : denujeme pomocí odvozovacích pravidel.
Rozli²ujeme 2 základní p°ístupy:
à la Church: termy obsahují explicitní anotace, kterými p°i°azujeme
typy prom¥nným v lambda abstrakcích. Podle anotací
pak odvozujeme typ termu.
à la Curry: pro daný term (bez anotací) odvozujeme jeho (moºný)
typ.
3/1
Typovaný lambda kalkulus
Osnova
Systém F à la Curry
Typovaný lambda kalkulus
Systém F à la Curry
Systém F
Dal²í názvy:
λ2
(GirardReynolds) polymorphic lambda calculus
the second-order lambda calculus
4/1
Typovaný lambda kalkulus
Systém F à la Curry
Typy v systému F
Denition (Typy systému F)
Bu¤
V
nekone£ná spo£etná mnoºina typových prom¥nných.
Mnoºina typ·
T
systému F je denována induktivn¥:
T = V | T → T | ∀VT
→ konstruuje funk£ní typy funkce z prvního typu do druhého.
∀ konstruuje polymorfní typy.
Konvence:
Typové prom¥nné ozna£ujme °eckými písmeny ze za£átku abecedy
(α,
β
atd.).
Typy ozna£ujme °eckými písmeny z prost°edku abecedy (τ ,
σ atd.).
σ1 → σ2 → σ3 pí²eme místo σ1 → (σ2 → σ3 )
∀ asociuje doprava: ∀α1 . . . ∀α .σ pí²eme místo
(∀α1 (∀α2 . . . (∀α (σ)) . . .)).
→ asociuje doprava:
n
n
5/1
Typovaný lambda kalkulus
Systém F à la Curry
Tvrzení v typovaných lambda kalkulech
6/1
Denition (tvrzení)
1
Tvrzení °íká, ºe daný term M
Zna£ení M
Typ
σ
∈Λ
je daného typu
σ ∈ T.
: σ.
je predikátem tvrzení a term M je subjektem tvrzení.
2
Deklarace je tvrzení, ve kterém je subjektem prom¥nná.
3
Báze (nebo téº kontext) je mnoºina deklarací, které mají za subjekty
r·zné prom¥nné. Zna£íme obvykle velkými °eckými písmeny (Γ,
Poznámka
V Haskellu relaci : zapisujeme pomocí znaku dvou dvojte£ek
Tvrzení M
:σ
tedy zapí²eme jako M
:: σ .
::
.
∆).
Typovaný lambda kalkulus
Systém F à la Curry
P°i°azení typ· v systému F
Denition
P°i°azení typ· v systému F je denováno následujícím systémem p°irozené
dedukce:
7/1
Typovaný lambda kalkulus
Systém F à la Curry
Pravidla (axiomy) pro p°i°azení typ· v systému F
(startovací pravidlo)
(eliminace
→)
(zavedení
Γ ` M : (σ → τ )
Γ`N:σ
Γ ` (MN ) : τ
→)
(eliminace
(zavedení
8/1
∀)
(x : σ) ∈ Γ
Γ`x :σ
∀)
Γ, x : σ ` M : τ
Γ ` (λx .M ) : (σ → τ )
Γ ` M : (∀α.σ)
Γ ` M : (σ[α := τ ])
Γ`M:σ
Γ ` M : (∀α.σ)
,
α 6∈ FV (Γ)
Typovaný lambda kalkulus
Systém F à la Curry
V¥ta o substituci v systému F
9/1
Lemma (o substituci v systému F)
1
Γ`M:σ
2
Pokud
pak
Γ, x : σ ` M : τ
D·kaz.
[
Γ[α := τ ] ` M : σ[α := τ ].
Barendregt92].
a
Γ`N:σ
pak
Γ ` M [x := N ] : τ .
Typovaný lambda kalkulus
Systém F à la Curry
V¥ta o redukci subjekt· v systému F
Theorem (o redukci subjekt· v systému F)
0
Bu¤ M β M . Pak v systému F platí, ºe pokud
D·kaz.
[
Barendregt92].
10/1
Γ`M:σ
pak
Γ ` M 0 : σ.
Typovaný lambda kalkulus
Systém F à la Curry
Silná normalizace v systému F
Theorem (o silné normalizaci pro systém F)
Jestliºe v systému F
Γ`M:σ
pak M je siln¥ normalizující.
D·kaz.
[
Barendregt92].
D·sledek
Systém F není turingovsky úplný, protoºe obsahuje jen totální funkce.
Systém F neobsahuje obecnou rekurzi.
Pokud n¥jaký systém obsahuje obecnou rekurzi (nap°. je v n¥m
typovatelný kombinátor Y ) tak obsahuje funkce, které nejsou totální
(nap°íklad YI nemá nf ). Takový systém proto není ani siln¥ ani slab¥
normalizující.
11/1
Typovaný lambda kalkulus
Systém F à la Curry
Kontrola typu, typovatelnost, obydlenost typu
Denition
Kontrola typu (type checking): Dáno M a
Zna£ení M
σ,
taková, ºe
` M : σ?
existuje M takový, ºe
` M : σ?
12/1
σ
:?.
Obydlenost (inhabitation): Dáno
Zna£ení
` M : σ?
: σ?.
Typovatelnost (typability): Dáno M , existuje
Zna£ení M
platí
? : σ.
σ,
Typovaný lambda kalkulus
Typy a nerozhodnutelnost I
Theorem (Joe B. Wells)
V systému F nelze rozhodnout:
13/1
1
kontrolu typu,
2
typovatelnost,
3
obydlenost.
Systém F à la Curry
Typovaný lambda kalkulus
Systém F à la Curry
Typy a nerozhodnutelnost II
D·kaz.
D·kaz, ºe v F je typovatelnost ekvivalentní kontrole typu byl znám uº
d°íve, viz. [
Barendregt92].
Barendregt92].
D·kaz nerozhodnutelnosti obydlenosti viz. [
D·kaz, ºe typovatelnost v F je nerozhodnutelná
viz. [
Wells-TypabilityL2].
Poznámka
Nerozhodnutelnost obydlenosti a ekvivalence typovatelnosti a kontroly typu
byly známy jiº pom¥rn¥ dlouho, ale chyb¥l stále d·kaz (ne)rozhodnutelnosti
typovatelnosti a kontroly typu F . Tyto dva problémy byly proto nazývány
embarrassing open problems, neº je Wells vy°e²il.
14/1
HindleyMilner·v algoritmus
Osnova
HindleyMilner·v algoritmus
Rank-k polymorsmus
15/1
V systému F se mohou kvantikátory typ· objevovat libovoln¥ v
typech.
Ukázalo se, ºe to ovliv¬uje rozhodnutelnost typovatelnosti.
HindleyMilner·v algoritmus
Rank-k polymorsmus
V systému F se mohou kvantikátory typ· objevovat libovoln¥ v
typech.
Ukázalo se, ºe to ovliv¬uje rozhodnutelnost typovatelnosti.
Denition
Bu¤ dáno k
∈ N.
Pak typ je ranku k (£asto psáno rank-k ) pokud se ºádný
jeho kvantikátor neobjevuje nalevo od více neº k
typ jako strom).
15/1
−1
²ipek (nakreslíme-li
HindleyMilner·v algoritmus
Rank-k polymorsmus
Example
∀αβ.α → β → α je rank-1.
(∀α.α → α) → (∀β.β → β)
je rank-2.
Example
Typ
∀α.α → (∀β.β)
(je ekvivalentní typu
Typ
16/1
(rank-1) není obydlený totální funkcí;
∀αβ.α → β ).
(∀α.α) → (∀β.β)
(rank-2) je obydlený totální funkcí
λ x .x .
HindleyMilner·v algoritmus
Rank-k polymorsmus
Odvoditelnost typ·
Pro rank-1 typy lze odvozovat typy (HindleyMilner·v
algoritmus [
damas1982principal]).
kfoury1992type,
Pro rank-2 lze také je²t¥ odvozovat typy [
kfoury1994direct].
Pro rank-k , k
17/1
>2
je odvoditelnost nerozhodnutelná.
HindleyMilner·v algoritmus
Osnova
HindleyMilner·v typový systém
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Jazyk HindleyMilnerova typového systému
Termy:
e
:= x | e1 e2 | λx .e |
let x
= e1 in e2
Typy:
τ := α | ι | τ → τ
Typová schémata:
σ := τ | ∀α.σ
18/1
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Konvence zna£ení
Budeme pouºívat následující konvenci zna£ení:
x pro lambda prom¥nné,
e pro lambda termy,
α
pro typové prom¥nné,
τ
pro typy,
ι
pro primitivní typy (jako nap°. Int apod.),
σ
pro typová schémata.
Sekvenci objekt· zna£me pro zjednodu²ení zápisu £arou, nap°íklad:
λx .M
místo
λx1 , . . . , xn .M , ∀α.τ
místo
∀α1 . . . ∀αn .τ
Sekvence m·ºe být pokaºdé jiná a jinak dlouhá.
19/1
atd.
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Volné prom¥nné
FTV(α)
FTV(τ
→τ ) =
FTV(∀ατ )
20/1
= {α}
0
=
FTV(τ )
∪ FTV(τ 0 )
FTV(τ )
\ {α}
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Uspo°ádání na typových schématech
Denition
βi 6∈ FTV(∀α.τ )
τ 0 = [τ /α]τ
∀α.τ > ∀β.τ 0
Slovy:
21/1
Dosadíme za kvantikované prom¥nné n¥jaké typy
τ1 , . . . , τn .
Kvantikujeme libovoln¥ ty prom¥nné, které nebyly volné v p·vodním
typovém schématu
∀α.τ .
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Uspo°ádání na typových schématech
Denition
βi 6∈ FTV(∀α.τ )
τ 0 = [τ /α]τ
∀α.τ > ∀β.τ 0
Slovy:
Dosadíme za kvantikované prom¥nné n¥jaké typy
τ1 , . . . , τn .
Kvantikujeme libovoln¥ ty prom¥nné, které nebyly volné v p·vodním
typovém schématu
∀α.τ .
Pozorování:
Relace
>
Je-li
je reexivní a tranzitivní, je to tedy uspo°ádání
σ > σ 0 znamená, ºe σ je obecn¥j²í
σ > σ 0 pak FTV(σ) ⊆ FTV(σ 0 ).
Intuitivn¥
typ neº
σ0.
Example
∀α.α → α > ∀β.(β → β) → (β → β) > (γ → γ) → (γ → γ)
21/1
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Substituce
Substituce na typech je denována obvyklým zp·sobem.
U typových schémat substituce pracuje pouze na volných prom¥nných,
vázané prom¥nné nechává.
Zna£ení S
22/1
= [τ1 /α1 . . . , τn /αn ],
nebo jen S
= [τ /α].
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Substituce
Substituce na typech je denována obvyklým zp·sobem.
U typových schémat substituce pracuje pouze na volných prom¥nných,
vázané prom¥nné nechává.
Zna£ení S
= [τ1 /α1 . . . , τn /αn ],
nebo jen S
= [τ /α].
Substituce si v²ímá jen volných prom¥nných, a
> si v²ímá jen vázaných prom¥nných.
22/1
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Substituce
Substituce na typech je denována obvyklým zp·sobem.
U typových schémat substituce pracuje pouze na volných prom¥nných,
vázané prom¥nné nechává.
Zna£ení S
= [τ1 /α1 . . . , τn /αn ],
nebo jen S
= [τ /α].
Substituce si v²ímá jen volných prom¥nných, a
> si v²ímá jen vázaných prom¥nných.
Platí proto, ºe
22/1
σ > σ0
pak S σ
> S σ0.
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Kontexty
Denition
Bu¤
Γ = hx1 : σ1 , . . . , xn : σn i.
S
FTV(Γ) :=
FTV(σi )
i
SΓ
Denujme
:= hx1 : S σ1 , . . . , xn : S σn i
Γ(τ ) := ∀α.τ ,
kde
α = FTV(τ ) \ FTP (Γ).
Intuitivn¥, kvantikujeme v²echny volné prom¥nné, které nejsou
vázány kontextem.
Γx
23/1
bu¤ kontext
Γ,
z kterého odebereme deklarace týkající prom¥nné x .
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Hindley-Milner·v typový systém
Denition
V Hindley-Milnerov¥ typovém systému pí²eme, ºe
Γ`e:σ
jestliºe to lze
odvodit následujícími pravidly:
TAUT
INST
GEN
24/1
(x
Γ`x :σ
Γ`e:σ
Γ ` e : σ0
Γ`e:σ
Γ ` e : ∀α.σ
: σ ∈ Γ)
(σ
(α
COMB
Γ ` e : τ0 → τ
Γ ` e0 : τ 0
0
Γ ` (ee ) : τ
> σ0)
ABS
6∈ FTV(Γ))
LET
Γx , x : τ 0 ` e : τ
Γ ` (λx .e ) : τ 0 → τ
Γ`e:σ
Γx , x : σ ` e 0 : τ
Γ ` (let x = e in e 0 ) : τ
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Hindley-Milner·v algoritmus
Dáno
Γ
a e , algoritmus W hledá substituci S a typ
τ
takové, ºe S Γ
Dále platí:
Theorem (Korektnost W )
Jestliºe W (Γ, e ) najde
(S , τ )
pak existuje odvození S Γ
` e : τ.
Theorem (Úplnost W )
M¥jme
Γ,
e , a bu¤
Γ0
instance
Γ
a
σ
takové, ºe
1
W (Γ, e ) usp¥je; bu¤ W (Γ, e )
2
0
existuje substituce R taková, ºe Γ
Takový typ
τ
= (S , τ );
Γ0 ` e : σ .
a
= RS Γ
a R S Γ(τ )
nazýváme principiální typ termu e.
D·kaz.
damas1982principal], nebo
Viz. originální £lánek [
http://www.cs.ucla.edu/~jeff/docs/hmproof.pdf.
25/1
Pak:
> σ.
` e : τ.
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Unikace
Denition
26/1
Unikátor typ·
τ
a
τ0
je substituce S taková, ºe S τ
τ a τ 0 je unikátor
0
R τ = R τ , existuje T
= S τ 0.
Nejobecn¥j²í unikátor typ·
S takový, ºe pokud
pro substituci R platí, ºe
taková, ºe R
= T ◦ S.
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Unikace
Denition
Unikátor typ·
τ
a
τ0
je substituce S taková, ºe S τ
τ a τ 0 je unikátor
0
R τ = R τ , existuje T
= S τ 0.
Nejobecn¥j²í unikátor typ·
S takový, ºe pokud
pro substituci R platí, ºe
taková, ºe R
= T ◦ S.
Theorem (Robinson 1965)
Existuje-li unikátor dvou typ·
τ
a
τ0
pak existuje jejich nejobecn¥j²í
0
unikátor (zn. U(τ, τ )) a lze ho efektivn¥ po£ítat.
D·kaz.
Viz. [
26/1
robinson1965machine]. (Ud¥lat p°íklad.)
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
Hindley-Milner·v algoritmus
W (Γ, e )
e
e
= (S , τ ), kde:
= x a x : ∀α.τ 0 ∈ Γ, pak S je identická
kde βi jsou nové prom¥nné.
= e1 e2 :
substituce a
τ = [β/α]τ 0 ,
bu¤
W (Γ, e1 )
e
= (S1 , τ1 ),
W (S1 Γ, e2 ) = (S2 , τ2 ) a
V = U(S2 τ1 , τ2 → β), kde β je nová
Pak S = V ◦ S2 ◦ S1 a τ = V β .
e = λx .e1 : nech´ β je nová prom¥nná, a bu¤
W (Γx , x : β, e1 ) = (S1 , τ1 ).
Pak S = S1 a τ = S1 (β) → τ1 .
= (let x = e1 in e2 ) : bu¤
W (Γ, e1 ) = (S1 , τ1 ) a bu¤
W (S1 Γx , x : S1 Γ(τ1 ), e2 ) = (S2 , τ2 ).
Pak S = S2 ◦ S1 a τ = τ2 .
prom¥nná.
Není-li spln¥ná n¥která z podmínek daného bodu, algoritmus selºe.
27/1
HindleyMilner·v algoritmus
HindleyMilner·v typový systém
let výrazy
Nutnost
let
výraz·
Example
Term
let x
(λx → M ) N není z hlediska typovacího
= N in M (i kdyº semanticky je):
1
Výraz
let x = λz → z in x
2
Výraz
(λx → x x ) (λz → z )
x má typ
systému ekvivalentní
(a → a).
nemá typ.
(a → a), který je ve výrazu x x
((a → a) → (a → a)) a v druhém na (a → a).
V prvním p°ípad¥ má x polymorfní typ
instanciován v prvním x na
V druhém p°ípad¥ nelze takto instanciovat typ x .
28/1
HindleyMilner·v algoritmus
Osnova
Rekurze v Hindley-Milnerov¥ typovém systému
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
Rekurzivní typy
Hindley-Milner·v typový systém neumoº¬uje rekurzivní
Nap°íklad
29/1
let x = x in x
let výrazy.
nejde typovat. (Cvi£ení: pro£?)
HindleyMilner·v algoritmus
e²ení 1: Kombinátor
Rekurze v Hindley-Milnerov¥ typovém systému
Y
M·ºeme p°idat kombinátor Y jako primitivní funkci s typem
∀α.(α → α) → α.
Problém: Není z°ejmé, jak se bude typový systém a algoritmus
odvození chovat.
Rekurze není sou£ástí typového systému.
30/1
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
e²ení 2: Pravidlo pro uniformní rekurzi
Do jazyka p°idáme dal²í syntaktickou konstrukci pro uniformní rekurzi
(téº zvanou monomorfní):
x x .e
Konstrukce x x .e nahrazuje Y (λx .e ).
P°idáme pravidlo:
1
(FIX-U)
1
31/1
Symbol
τ
Γx , x : τ ` e : τ
Γ ` x x .e : τ
zna£í podle konvence typy, ne typová schémata!
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
e²ení 2 problémy I
Rekurzivní funkce nemohou volat samy sebe s jiným typem v rekurzi.
Nap°íklad:
data Seq a = Nil | Seq a (Seq (a, a))
:: Seq a → Int
size Nil = 0
s ) = 1 + 2 ∗ size
size (Seq
size
nelze zapsat pomocí x.
32/1
s
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
e²ení 2 problémy II
P°i n¥kterých vícenásobných rekurzích vycházejí mén¥ obecné typy.
Nap°íklad:
f
= let
0
f x = x
0
0
g y = f 3
in f 0
33/1
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
e²ení 2 problémy II
P°i n¥kterých vícenásobných rekurzích vycházejí mén¥ obecné typy.
Nap°íklad:
f
= let
0
f x = x
0
0
g y = f 3
in f 0
Zkracujme typ páru jako
(τ, τ 0 )
a zkracujme pair e1 e2 jako
(e1 , e2 )
.
P°i p°episu dvojnásobné rekurze pomocí páru dostáváme:
(f , g ) = (x p . ((λx .x ), (λy .(rst p )3)))
|
{z
}
Ozna£ený term je typu
(α → α, β → γ).
První funkce musí být aplikovatelná na 3, takºe
γ musí být α. Takºe typ abychom
typ být (Int → Int , β → Int ).
Výsledný typ f tak bude Int → Int .
zárove¬
33/1
α
musí být Int a
mohli pouºít FIX-U, musí
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
e²ení 3: Polymorfní pravidlo pro rekurzi
mycroft1984polymorphic].
Polymorfní rekurzi rozpracoval poprvé [
2
Polymorfní rekurzi denuje pravidlo:
Γx , x : σ ` e : σ
Γ ` x x .e : σ
(FIX-P)
K algoritmu pro odvození principiálního typu p°idáme:
e
= x x .e1
bu¤
σ0 = ∀β.β
Γ0 = Γx ∪ {x : σ0 }
opakujeme:
(S +1 , τ +1 ) = W (Γ , e1 )
σ +1 = S +1 Γ (τ +1 )
Γ +1 = (S +1 Γ ) ∪ {x : σ +1 }
i
i
i
i
i
i
i
i
i
i
x
6= σi +1 .
= Si +1 . . . S1 a τ = τi +1 .
dokud Si +1 σi
Pak S
2
34/1
i
Rozdíl: zde uº pravidlo obsahuje typová schémata.
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
Polymorfní rekurze v na²em p°íkladu
Hledejme typ výrazu x p .((λx .x ),
(λy .(rst p )3)).
Γi = {p : σi } a σi nemají volné prom¥nné.
Si +1 Γi (τi +1 ) okvantikuje v²echny prom¥nné τi +1 .
V na²em p°ípad¥ je vºdy
Proto Si +1 Γi
= Γi
a
1
σ0 = ∀ω.ω ,
2
= [(Int → α, β)/ω],
τ1 = (γ → γ, δ → α),
σ1 = ∀αγδ.(γ → γ, δ → α),
3
= [Int /γ],
τ2 = ( → , ζ → Int ),
σ2 = ∀ζ.( → , ζ → Int ),
4
= [Int /],
τ3 = (η → η, θ → Int ),
σ3 = ∀ηθ.(η → η, θ → Int ) = S3 σ2 ,
S1
S2
S3
τ = τ3 = (η → η, θ → Int ).
FTV(Γ) = {}.)
Kýºený principiální typ výrazu x p . . . . je tedy
(Výsledná substituce je nezajímavá, nebo´
35/1
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
Rozhodnutelnost odvození typ· s polymorfní rekurzí
36/1
Na n¥kterých termech se algoritmus zacyklí.
.λx .f , protoºe bude
σn = ∀α0 . . . αn .α0 → . . . → αn .
Nap°íklad na x f
vycházet
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
Rozhodnutelnost odvození typ· s polymorfní rekurzí
36/1
Na n¥kterých termech se algoritmus zacyklí.
.λx .f , protoºe bude
σn = ∀α0 . . . αn .α0 → . . . → αn .
Nap°íklad na x f
vycházet
P°idání polymorfní rekurze £iní Hindley-Milner·v systém
nerozhodnutelný henglein1993type.
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
Rozhodnutelnost odvození typ· s polymorfní rekurzí
Na n¥kterých termech se algoritmus zacyklí.
.λx .f , protoºe bude
σn = ∀α0 . . . αn .α0 → . . . → αn .
Nap°íklad na x f
vycházet
P°idání polymorfní rekurze £iní Hindley-Milner·v systém
nerozhodnutelný henglein1993type.
Proto je nutné v n¥kterých p°ípadech explicitn¥ typovat.
Nap°íklad pro
data Seq a = Nil | Seq a (Seq (a, a))
:: Seq a → Int
=0
size (Seq
s ) = 1 + 2 ∗ size
size
size Nil
s
Haskell vyºaduje explicitní typ pro size .
36/1
HindleyMilner·v algoritmus
Rekurze v Hindley-Milnerov¥ typovém systému
Poznámky
Vztah mezi uniformní a polymorfní rekurzí je podobný
jako mezi
(λx .e )e 0
a let x
= e 0 in e .
Jakmile p°idáme kterýkoliv ze zp·sob· zavád¥jící obecnou rekurzi,
nem·ºe být typový systém ani siln¥ ani slab¥ normalizující.
37/1
HindleyMilner·v algoritmus
Osnova
Unika£ní algoritmus
HindleyMilner·v algoritmus
Unika£ní algoritmus
Unika£ní algoritmus
Popí²eme algoritmus, který vºdy najde nejobecn¥j²í unikátor (MGU)
dané mnoºiny výraz·, existuje-li.
Více viz. [
baader2001unication].
(Efektivn¥j²í algoritmus byl navrºen v [
38/1
martellimontanari1982].)
HindleyMilner·v algoritmus
Unika£ní algoritmus
Nesouhlasící mnoºina
Denition (nesouhlasící mnoºina)
Bu¤
W = {E1 , . . . , E } mnoºina r·zných výraz· a bu¤ k
n
délka úseku
zleva, který je stejný u v²ech Ei . Bu¤
D = {D | 1 6 i 6 n, D
i
i
je pod-výraz Ei za£ínající na k
+ 1.
D nazveme nesouhlasící mnoºinou W.
Example
Pro
W = {P (x , f (y , z )), P (x , |{z}
a ), P (x , g (h (k (x ))))}
| {z }
bude
39/1
|
D = {f (y , z ), a, g (h(k (x )))}
{z
}
pozici}
HindleyMilner·v algoritmus
Unika£ní algoritmus
Unika£ní algoritmus
1
2
= 0, W0 = W
Volme k
Je-li
|Wk | = 1,
a S0
= [].
skon£íme; Sk je MGU
W.
V opa£ném p°ípad¥ najdeme nesouhlasící mnoºinu
3
Jestliºe existuje prom¥nná xk
∈ Dk
a term tk
D
∈ Dk
nevyskytuje v tk , pokra£ujeme následujícím krokem.
W není unikovatelná.
Volme S +1 = [t /x ] ◦ S a W +1 = [t /x ]W
(£ili W +1 = S +1 W).
Poloºme k = k + 1 a jd¥me do ??.
Pokud ne, skon£íme;
4
k
k
5
k
k
k
k
k
k
k
k
Example
Najd¥te MGU
40/1
W = {P (a, x , f (g (y ))), P (z , f (z ), f (u ))}.
k
pro
W
k.
takové, ºe xk se
HindleyMilner·v algoritmus
Unika£ní algoritmus
V¥ty o unika£ním algoritmu
Theorem
Pro kone£nou neprázdnou mnoºinu výraz·
W algoritmus vºdy skon£í.
D·kaz.
V k -tém kroku mnoºina Sk +1
mnoºina Sk
W.
W obsahuje o jednu prom¥nnou mén¥ neº
Theorem (V¥ta o unikaci)
Je-li
W neprázdná unikovatelná mnoºina výraz·, pak unika£ní algoritmus
najde MGU této mnoºiny.
41/1
HindleyMilner·v algoritmus
Unika£ní algoritmus
D·kaz v¥ty o unikaci
D·kaz.
W. Ukáºeme, ºe v kaºdém T = T ◦ S ,
W = TS W.
Zkoumejme ??. krok algoritmu v k -té iteraci. Jelikoº T = T ◦ S
unikuje W, unikuje T mnoºinu D (nesouhlasící mnoºina pro S W).
D tedy musí obsahovat n¥jakou prom¥nnou x a term t r·zný od x
Bu¤ T libovolný unikátor
tedy T
k
k
k
k
k
a Txk
k
k
= Ttk .
k
coº nelze. Algoritmus tedy neskon£í a pokra£uje do kroku
Nech´ algoritmus volí Sk +1
T
nebo´ Txk
42/1
k
Pokud by tk obsahoval xk pak by Ttk obsahoval Txk ,
= Ttk
= [tk /xk ] ◦ Sk .
Pak
◦ Sk +1 = (T ◦ [tk /xk ]) ◦ Sk = T ◦ Sk
a tk neobsahuje xk .
??.
Typový systém Haskellu
Osnova
Typový systém Haskellu
Hindley-Milner·v typový systém v Haskellu
43/1
Haskell 98 pouºívá HM typový systém s polymorfní rekurzí.
V²echy typy jsou implicitn¥ univerzáln¥ kvantikované.
3
Kontext není uºivateli p°ístupný.
Nelze proto specikovat typ s prom¥nnou vázanou v kontextu.
Nap°íklad:
function
:: (Int → a) → (a, a)
=
function f
let
t
=f 4
in (t , t )
Zde nelze explicitn¥ otypovat vno°enou funkci t . GHC hlásí:
Couldn't match expected type `a1' against inferred type `a'
`a1' is a rigid type variable bound by the type signature for `t' at ...
`a' is a rigid type variable bound by the type signature for `function' at ...
3
V GHC 7 to p·jde pomocí pragma
ScopedTypeVariables.
Typový systém Haskellu
Syntaxe jazyka Haskell
Kompletní syntaxi Haskellu popisuje Haskell 98 Language and Libraries,
AKA The Haskell 98 Report.
44/1
TODO odkaz
Cvi£ení
Osnova
Cvi£ení
Cvi£ení I
Cvi£ení
Odvo¤te z axiom· Hindley-Milnerova typového systému principiální typy
t¥chto výraz·:
1
λx → x
2
λx
y
3
λx
y z
4
let x = λz → z in x
5
(λx → x x ) (λz → z )
(kombinátor I )
→x
(kombinátor K )
→ (x z ) (y z )
(kombinátor S )
x
pop°ípad¥ ukaºte, pro£ typ nemají.
Cvi£ení
Implementujte Hindler-Milner·v algoritmus.
45/1
Literatura
Osnova
Literatura
Literatura I
46/1
Download

Funkcionální programování - Typovaný lambda