Slidy_2006

[ Char ] → Bool )
typ’ (∅ , elem ’*’ "-*-") = ( ρ 3 ◦ ρ 2 ◦ ρ 1 , ρ 3 β ) , kde
ρ 1 = [[ Char ] → Bool /β ], τ = [ Char ] → Bool
ρ 2 = id, ϕ = [ Char ]
ρ 3 = mgu ([ Char ] → Bool )([ Char ] → γ ) = [B ool /γ ]
tj. ([[ Char ] → Bool /β , Bool /γ ], Bool ])
76
Význam typo vání
• v ˇcasná detekce v ˇetšin y prog r amo vých ch yb
• pro oper ace s hodnotami známých typ ˚u lz e genero v at ef ektivn ˇejší kód
• dokumentace
77
P oužití v typo v aných jazycích
• typ , který uživ atel nedeklar uje , je odv oz en a použit
• typ , který uživ atel deklar uje je také odv oz en a zk ontroluje se , zda je stejný nebo
obecn ˇejší než deklaro v aný; deklaro v aný je použit
78
K ombinátor y S ,K,I
S f g x ˆ S f x ( g x )
K x y ˆ K x
I x ˆ I x
S :: ( α → β → γ ) → ( α → β ) → α → γ
K :: α → β → α
I :: α → α
S ≈ λf λg λx.f x ( g x )
K ≈ λxλy .x
I ≈ λx.x
79
Def: K ombinátoro vý ter m je ter m obsahující pouz e k ombinátor y (S ,K,I) a aplikace .
Def: K ombinátoro vá redukce
S M N P ˆ S M P ( N P )
K M N ˆ K M
I M ˆ I M
ˆ je k ompatibilní uzáv ˇer ˆ S ∪ ˆ K ∪ ˆ I
∼ je refle xivní, symetr ic ký a tr anzitivní uzáv ˇe relace ˆ
80
V ˇeta: ∼ ⊆ ≈
P ˇridání pr a vidla e xtensionality:
∀ P .M P ∼ prime N P
M ∼ prime N
M ∼ N
M ∼ prime N
V ˇeta: ∼ prime ⊆ ≈
V ˇeta: Každý uza v ˇrený λ − ter m M lz e p ˇre vést na ≈ − ekviv alentní k ombinátoro vý
ter m N .
81
K ombinátoro vá báz e je nejmenší (vzhledem k inkluzi) množina k ombinátor ˚u, jimiž lz e
vyjád ˇrit všechn y uza v ˇrené λ -ter m y .
P oznámka: Jelik ož I ≈ S K K , plyne z V ˇety , že { S , K } je k ombinátoro vá báz e .
V ˇeta: { K , S } je k ombinátoro vá báz e .
D ˚ukaz:
(i) Každý uza v ˇrený ter m lz e vyjád ˇrit pomocí S , K , I
(ii) I ≈ S K K
(iii) S nelz e vyád ˇrit pomocí K
(iv) K nelz e vyád ˇrit pomocí S
82
P ˇríklad: Necht ’ X je k ombinátor defino v aný pr a vidlem X M ˆ M K S K .
P ak { X } je k ombinátoro vá báz e .
D ˚ukaz:
X X X ˆ X K S K X ˆ K K S K S K X ˆ K K S K X ˆ K K X ˆ K
X ( X X ) ˆ X X K S K ˆ X K S K K S K ˆ K K S K S K K S K ˆ K K S K K S K ˆ
K K K S K ˆ K S K ˆ S
83
V netypo v aném k ombinátoro vém kalkulu lz e vyjád ˇrit k ombinátor pe vného bodu:
Y = S ( C B ( S I I )) ( C B ( S I I ))
84
Sem pat ˇrí str an y 55, 56, 57, 58.
Curr yho-Ho w ard ˚uv isomorfism us , g r af o vá redukce , optimalizace k ombinátoro vé sady .
85
S ( K P ) Q ⇒ B P Q
S P ( K Q ) ⇒ C p Q
S ( K P ) ( K Q ) ⇒ K ( P Q )
86
S ( K P ) Q M ˆ K P M ( Q M ) ˆ P ( Q M )
B P Q M ˆ P ( Q M )
S P K Q M ˆ P M ( K Q M ) ˆ P ( M Q )
C P Q M ˆ P M Q
S ( K P ) ( K Q ) M ˆ K P M ( K Q M ) ˆ 2 P Q
K ( P Q ) M ˆ P Q
Další vylepšení:
S ( K P ) I ⇒ P
η -redukce:
87
Vyjád ˇrení jednosm ˇer ného k ombinátor u pe vného bodu v SKIBC
= S I (B (S I) (S I I) (B (S I) (S I I)))
F = S I (B (S I) (S I I) (B (S I) (S I I))) F
ˆ F (B (S I) (S I I) (B (S I) (S I I)) F )
ˆ F (S I (S I I (B (S I) (S I I))) F )
ˆ F (S I (B (S I) (S I I) (B (S I) (S I I))) F )
= F ( F )
88
Super k ombinátor y
Motiv ace pro λ -lifting:
P = ( λx. (+) x (( λy .(∗ ) x y ) 3)) 4
Q = ( λxy .(+) x ( (∗ ) x y ) ) 4 3
P ∼ prime Q , ale p ˇreklad Q do k ombinátor ˚u je snažší než p ˇreklad P .
89
Super k ombinátor y
Idea: Každém u ter m u (funkcionálním u prog r am u) ušít na mír u „ jeho “ sadu k ombinátor ˚u -
tzv . super k ombinátor ˚u. P ˇrepiso v ací pr a vidlo pro každý super k ombinátor lz e
implemento v at jak o podprog r am v cílo vém jazyce (strojo vém nebo b yto vém kódu).
Def: Uza v ˇrený ter m S = λx 1 λx 2 . . . λx n .E je super k ombinátor když
n ≥ 0
E není λ -abstr akce
všechn y λ -abstr akce v E jsou super k ombinátor y
ˇCíslo n je tzv . ar ita super k ombinátor u S .
90
Super k ombinátoro vý rede x je tv ar u S M 1 M 2 . . . M n .
Reduk ˇcní pr a vidlo S x 1 x 2 . . . x n ˆ E neobsahuje v olné prom ˇenné, takže ho lz e
vyjád ˇrit pe vným podprog r amem v cílo vém kódu...G stroj.
Def: Super k ombinátor y ar ity 0 se nazýv ají k onstantní aplikativní for m y (CAF).
P ˇríklady super k ombinátor ˚u
α = 3 α = 3
β = (+) 25 β = (+) 25
γ = λx.x γ x = x
δ = λx. (+) x 1 δ x = (+) x 1
ε = λx. (∗ ) x x ε x = (∗ ) x x
ζ = λxλy .(− ) y x ζ x y = (− ) y x
η = λf .f ( λx. (∗ ) x x η f = f epsilon1
91
P ˇríklady nesuper k ombinátor ˚u
λx.y není uza v ˇrený
λy .(− ) y x není uza v ˇrený
λf .f ( λx.f x 2) vnit ˇrní abstr akce není super k ombinátor (není uza v ˇrená)
λx.x ( λy .y ( λz .z y )) nejvnit ˇrn ˇejší abstr akce není super k ombinátor (není uza v ˇrená)
92
Algor itm us p ˇre v odu λ -ter m u do super k ombinátoro vého prog r am u
Algor itm us: S C
Vstup: ter m M
Výstup: dv ojice ( D , M ) , kde D je množina definic super k ombinátor ˚u
M je super k ombinátoro vý ter m ekviv alentní M
S C ( M ) = T (∅ , M )
T ( D , M ) = jestliže M neobsahuje žádnou λ -abstr akci
pak ( D , M )
jinak T ( D ∪ { " α x 1 . . . x n x = N " } , M prime)
kde λx.N je ne vnit ˇrn ˇejší abstr akce v M
{ x 1 , . . . , x n } = FV ( λx.N )
M prime vznikne z M náhr adou abstr akce λx.N ter mem α x 1 . . . x n
P oznámka: Krok ˚um tr ansf or mace T se ˇríká „ vynášení lambda “ (lambda-lifting).
93
Sem pat ˇrí str ana 65.
P ˇríklad.
94
V ˇeta: Algor itm us p ˇre v odu λ -ter m u do super k ombinátoro vého ter m u k on v erguje a
výsledný ter m M je (p ˇri definicích z D ) ekviv alentní p ˚uv odním u ter m u M .
D ˚ukaz:
K on v ergence – v každém kroku ub ude λ -abstr akce , algor itm us k on ˇcí, když v ter m u už
žádné abstr akce nejsou. Každý krok zacho vává ekviv alenci:
λx.N ≈ λx.α x 1 . . . x n x (protože „α x 1 . . . x n x = N “ p ˇridáváme do D ), takže
λx.N ≈ λx.α x 1 . . . x n (po η -redukci)
95
V ˇeta: P ˇri p ˇre v odu λ -ter m u M v elik osti k do super k ombinátoro vého ter m u M b ude
mít ter m M v elik ost nejvýše k a celk o vá v elik ost všech ter m ˚u v D b ude v O ( k ) .
D ˚ukaz:
1. ter m α x 1 . . . x n není delší než λx.N , protože všechn y v olné prom ˇenné
x 1 , . . . , x n se v N vyskytují.
2. v každém kroku je p ˇrír ustek k celk o vé v elik osti nejvýše ro v en po ˇctu v olných
prom ˇenných ter m u N .
96
Sem pat ˇrí str an y 67 a 68.
97
Modifikace vynášecího algor itm u na pln ˇe líné vynášení
Def: P odvýr az M abstr akce L je v olný, když všechn y prom ˇenné v M jsou v olné v L .
Maximální v olný výr az v L je tak o vý v olný výr az, který není vlastním podter mem
žádného výr azu v olného v L .
P ˇríklad: λxλy .y + sq r tx
Ab y b ylo zar u ˇceno , že po lambda-vynesení b ude zacho vána plná lenost, je n utné
vynášet místo v olných prom ˇenných maximální v olné výr azy .
98
Sem pat ˇrí str ana 70.
Vynášení z lokálních definic.
99
Monády
100
class F unctor f where
f map :: a → b → f a → f b
instance F unctor M ay be where
f map f N othing = N othing
f map f ( J ust x ) = J ust ( f x )
instance F unctor [ ] where
f map = map
instance F unctor I O where
f map f x = x greatermuch = r etur n ◦ f
101
class M onad m where
r etur n :: a → m a
(greatermuch =) :: m a → ( a → m b ) → m b
(greatermuch ) :: m a → m b → m b
f ail :: S tr ing → m a
p greatermuch q = p greatermuch = const q
f ail = er r or
instance M onad M ay be where
r etur n = J ust
N othing greatermuch = k = N othing
J ust x greatermuch = k = k x
f ail s = N othing
102
instance M onad [ ] where
r etur n = (: [ ])
[ ] greatermuch = f = [ ]
( x : s ) greatermuch = f = f x + + ( s greatermuch = f )
f ail s = [ ]
instance M onad I O where
r etur n = pr imr etI O
(greatermuch =) = pr imbindI O
103
Monadic ké axiom y
r etur n a greatermuch = k = k a
m greatermuch = r etur n = m
m greatermuch = ( λx → k x greatermuch = h ) = ( m greatermuch = k ) greatermuch = h
104
f map :: ( a → b ) → ( M a → M b )
f map f m = m greatermuch = r etur n ◦ f
j oin :: M ( M a ) → M a
j oin z = z greatermuch = id
P ˇríklad: Seznamo vá monáda instance M onad [ ] where
r etur n = (: [ ])
[ ] greatermuch = k = [ ]
( x : s ) greatermuch = k = k x + + ( s greatermuch = k )
P otom j oin = concat, f map = map .
105
Monadic ké zák on y
f map id = id
f map ( f ◦ g ) = f map f ◦ f map g
f map f ◦ r etur n = r etur n ◦ f
f map f ◦ j oin = j oin ◦ f map ( f map f )
j oin ◦ r etur n = id
j oin ◦ f map r etur n = id
j oin ◦ f map j oin = j oin ◦ j oin
m greatermuch = k = j oin ( f map k m )
106
f map id = id
D ˚ukaz: Pro všechna m je
f map id m = m greatermuch = r etur n ◦ id
= m greatermuch = r etur n
= m
= id m
107
f map ( f ◦ g ) = f map f ◦ f map g
D ˚ukaz: Pro všechna m je
f map ( f ◦ g ) m = m greatermuch = r etur n ◦ f ◦ g
= m greatermuch = ( λx → r etur n ( f ( g x )))
= m greatermuch = ( λx → r etur n ( g x ) greatermuch = r etur n ◦ f )
= ( m greatermuch = r etur n ◦ g ) greatermuch = r etur n ◦ f
= f map g m greatermuch = r etur n ◦ f
= f map f ( f map g m )
= ( f map f ◦ f map g ) m
108
f map f ◦ r etur n = r etur n ◦ f
D ˚ukaz: Pro všechna m je
f map f ◦ r etur n m = f map f ( r etur n m )
= r etur n m greatermuch = r etur n ◦ f
= ( r etur n ◦ f ) m
j oin ◦ r etur n = id
D ˚ukaz: Pro všechna z je
j oin ◦ r etur n z = j oin ( r etur n z )
= r etur n z greatermuch = id
= id z
109
Aditivní monády
class M onad m where
(greatermuch =) :: m a → ( a → m b ) → m b
r etur n :: a → m a
(greatermuch ) :: m a → m b → m b
m greatermuch k = m greatermuch = λ _ → k
class
M onad m ⇒ M onadP lus m where
mz er o :: m a
mpl us :: m a → m a → m a → m a
110
Zák on y aditivních monád
m greatermuch mz er o = mz er o
mz er o greatermuch m = mz er o
m ‘mpl us ‘ mz er o = m
mz er o ‘mpl us ‘ m = m
111
P ˇríklady aditivních monád
instance M onadP lus M ay be where
mz er o = N othing
N othing ‘mpl us ‘ y = y
J ust x ‘mpl us ‘ _ = J ust x
instance M onadP lus [ ] where
mz er o = [ ]
mpl us = (++)
112
Str an y 80 a 81. Inter prety výr az ˚u.
113
Monadic ké k ombinátor y pro syntaktic k ou analýzu
ne wtype P ar ser a = P ( S tr ing → [( a, S tr ing )])
instance F unctor P ar ser where
f map f ( P p ) = P ( λinp → [( f v , out )|( v , out ) ← p inp ])
instance M onad P ar ser where
r etur n v = P ( λinp → [( v , inp )])
( P p ) greatermuch = f = P ( λinp → concat [pappl y ( f v ) out |( v , out ) ← p inp ])
r etur n je k onstantní parser , který vždy usp ˇeje (bez ˇctení vstupu).
greatermuch = vytvá ˇrí sekv ence z parser ˚u.
instance M onadP lus P ar ser where
mz er o = P ( λinp → [ ])
P p ‘mpl us ‘ P q = P ( λinp → p inp + + q inp ]
mz er o je n ulo vý parser , k etrý vždy selže .
mpl us vytvá ˇrí alter nativy z parser ˚u.
114
V ˇeta: T ypo vý k onstr uktor P ar ser spl ˇnuje monadic ké axiom y .
D ˚ukaz:
1. r etur n a greatermuch = k = k a
r etur n a greatermuch = k
= P ( λs → [( a, s )]) greatermuch = k
= P ( λs → concat [pappl y ( k v ) t|( v , t ) ← [( a, s )]])
= P ( λs → pappl y ( k a ) s )
= k a
2. P p greatermuch = r etur n = P p
P p greatermuch = r etur n
= P ( λs → concat [pappl y ( r etur nv ) t|( v , t ) ← p s ])
= P ( λs → concat [[( v , t )] |( v , t ) ← p s ])
= P ( λs → p s )
= P p
115
3. P p greatermuch = ( λx → k x greatermuch = h ) = ( P p greatermuch = k ) greatermuch = h
P p greatermuch = ( λx → k x greatermuch = h )
= P ( λs → concat [pappl y ( k v greatermuch = h ) t|( v , t ) ← p s ])
= P ( λs → concat [pappl y ( P ( λu → concat [pappl y ( h w ) y |( w , y ) ←
pappl y ( k v ) u ])) t|( v , t ) ← p s ])
= P ( λs → concat [concat [pappl y ( h w ) y |( w , y ) ←
pappl y ( k v ) t]|( v , t ) ← p s ])
= P ( λs → concat [pappl y ( h w ) y |( w , y ) ←
concat [pappl y ( k v ) t|( v , t ) ← p s ]])
= P ( λu → concat [pappl y ( k v ) t|( v , t ) ← p u ]) greatermuch = h
= ( P p greatermuch = k ) greatermuch = h
116
Aplikace parser u na ˇret ˇez ec
pappl y :: P ar ser a → S tr ing → [( a, S tr ing )]
pappl y ( P p ) s = p s
pak p greatermuch = h lz e vyjád ˇrit pomocí pappl y :
p greatermuch = h = P ( λx → concat [pappl y ( h v ) t|( v , t ) ← pappl y p s ])
Operátor „ deter minizace “
f ir st :: P ar ser a → P ar ser a
f ir st ( P p ) = P ( λs → case p s of
[ ] → [ ]
x : t → [x ]
Deter ministic ká alter nativ a
(+ + +) :: P ar ser a → P ar ser a → P ar ser a
p + + + q = f ir st ( p ‘mpl us ‘ q )
117
Sekv enci parser ˚u lz e zapsat
p 1 greatermuch = λx 1 →
p 2 greatermuch = λx 2 →
. . .
p n greatermuch = λx n →
r etur n ( f x 1 x 2 . . . x n )
nebo
do x 1 ← p 1
x 2 ← p 2
. . .
x n ← p n
r etur n ( f x 1 x 2 . . . x n )
P oznámka: V jistých v erzích Hask ellu e xisto v ala tzv . monadic ká comprehension:
[f x 1 x 2 . . . x n |x 1 ← p 1 , x 2 ← p 2 . . . , x n ← p n ]
118
Jednoduché parser y
P arser , který usp ˇeje na libo v olném znaku, pokud je na vstupu; na prázdném vstupu
selže .
item :: P ar ser C har
item = P λx → case s of
[ ] → [ ]
( x : t ) → [( x, t )]
119
Jednoduché parser y
sat :: ( C har → B ool ) → P ar ser C har
sat p = do x ← item
if p x then r etur n x
el se mz er o
char :: C har → P ar ser C har
char = sat ◦ (==)
dig it, low er , upper , letter , al phaN um :: P ar ser C har
dig it = sat isD ig it
low er = sat isLow er
upper = sat isU pper
letter = low er ‘mpl us ‘ upper
apl haN um = letter ‘mpl us ‘ dig it
120
str ing :: S tr ing → P ar ser S tr ing
str ing "" = r etur n ""
str ing ( x : s ) = do char x
str ing s
r etur n ( x : s )
121
K ombinátor y opak o v acích parser ˚u
many 1 :: P ar ser a → P ar ser [a ]
many 1 p = do x ← p
s ← many p
r etur n ( x : s )
many :: P ar ser a → P ar ser [a ]
many p = many 1 p + + + r etur n [ ]
nat :: P ar ser I nt
nat = many 1 dig it greatermuch = r etur n ◦ r ead
int :: P ar ser I nt
int = ( char prime− prime greatermuch nat greatermuch = r etur n ◦ neg ate ) + + + nat
122
ident :: P ar ser S tr ing
ident = do { x ← Low er ; s ← many al phanum ; r etur n ( x : s )}
spaces :: P ar ser ()
spaces = many 1 ( sat isS pace ) greatermuch r etur n ()
comment :: P ar ser ()
comment = str ing " − − " greatermuch many ( sat ( / = prime \ n prime)) greatermuch r etur n ()
j unk :: P ar ser ()
j unk = many ( spaces + + + comment ) greatermuch r etur n ()
tok en :: P ar ser a → P ar ser a
tok enp = do { v ← p ; j unk ; r etur n = v }
123
sy mbol :: S tr ing → P ar ser S tr ing
sy mbol = tok en ◦ str ing
identif ier :: [S tr ing ] → P ar ser S tr ing
identif ier k s = tok en ( do x ← ident
if x ‘el em ‘ k s
then mz er o
el se r etur n x
124
Str an y 91 - 106.
125