Comeback: Prolog je typový systém Haskellu
Pokud se oprostíme od několika detailů (např. od datových konstrukturů, polymorfismu a několika dalších drobností včetně rekurze), je typový systém Haskellu poměrně jednoduchý a popsatelný několika řádky Prologu. Kromě rekonstruování těchto několika řádek je cílem úkolu F ještě (trochu užitečnější) drobné opakování Prologu před zkouškovým.
Trochu zjednodušený Haskell
Předem, když odstraníte konstruktory, polymorfismus a rekurzi, zbyde vám z Haskellu jen obyčejný lambda kalkulus, tj. jazyk, ve kterém existují jen 3 věci:
- proměnně, v Haskellu
a, b, c, d, ...
- aplikace funkce na parametru, v haskellu
f a
(tedy i postupně na víc parametrů jako((f a) b) c ...
) - vyrobení funkce pomocí lambda abstrakce,
\x -> ....
- navíc tam budeme psát i závorky, ale to je syntaktická pomůcka nutná jen proto, že lidstvo miluje psaní do řádků
V lambda kalkulu přímo neexistují čísla, booleany, stringy, ani jiné datové typy, protože bez datových konstruktorů je vyrobit nejde. Kupodivu, i bez toho je to plnohodnotný programovací jazyk a jde v něm naprogramovat cokoliv, tj. i čísla, booleany a stringy.
Úkol, část 1
Vyrobte predikát parse_lambda/2
tak, aby platilo např.:
parse_lambda("\a -> \b -> b (b a)", lambda('a', lambda('b', app('b', app('b', 'a'))))).
Pro jednoduchost uvažujte jen proměnné vyrobené z jednoho malého písmene, jen lambdy s jednou abstrahovanou proměnnou, a whitespace neřešte (tj. výraz z příkladu můžete považovat za ekvivalentní "\a->\b->b(ba)"
.
Podobně jako v Haskellu, lambdová šipka platí “kam může”, tj. většinou až do konce závorky nebo do konce výrazu. Tj. \a -> a b
je vždycky \a -> (a b)
, nikoliv (\a -> a) b
.
Upozornění: aplikace funkcí jsou asociativní zleva, tj. aaa
je (aa)a
.
Typový systém
Pokud máte v ruce rozparsovaný lambda kalkulus, odvodit z něj typ jde už celkem jednoduše.
Nejdřív potřebujeme vyrobít jazyk typů. Ten se sestává jen z:
- typových proměnných (
a b c d ...
) - typu funkce (protože nic jiného nemáme), funkce z
a
dob
se zapíše tradičněa -> b
- závorek, aby se neřeklo
V Prologu typ funkce budeme reprezentovat pomocí struktury fun/2
a prologových proměnných, tj. např. typ a -> b -> b
budeme psát třeba jako fun(A, fun(B, B))
.
Při odvozování typu si musíte pamatovat, jakým datovým proměnným jste už přiřadili jaký typ. Takovou informaci ukládáte do tzv. kontextu, což je vlastně jen asociativní seznam, ve kterém k reálným proměnným přiřazujete typy.
V našem případě navíc zadarmo můžete uvažovat, že všechny výrazy jsou uzavřené, tj. každá proměnná ve výrazu je uvnitř nějaké lambdy, která ji zachycuje.
Pak to už jde jednoduše:
- Pokud ohodnocujete typ nějaké proměnné, prostě se podíváte do kontextu jestli tam má nějaké přiřazené typové ohodnocení, a ten typ vrátíte jako výsledek.
- Pokud ohodnocujete typ lambdy, tj.
lambda('a', Vyraz)
, tak:- do kontextu přidáte informaci o tom, že ‘a’ má nějaký typ (třeba
X
, obecně prostě novou prologovou proměnnou) - s novým kontextem zjistíte rekurzivně typ výrazu
Vyraz
, vyjde vám typT
- celá lambda má následně typ funkce z
X
(protože to je typ parametru) doT
(protože to je typ výsledku), tedyfun(X,T)
.
- do kontextu přidáte informaci o tom, že ‘a’ má nějaký typ (třeba
- Pokud ohodnocujete typ aplikace
app(Funkce,Parametr)
, pak:- Rekurzivně se zavoláte na výraz
Funkce
, vyjde vám typ funkceTF
- Rekurzivně se zavoláte na výraz
Parametr
, vyjde vám typ parametruTP
- Víte, že funkce typu
TF
přijala parametr typuTP
a musí vrátit nějaký typ výsledkuTV
. Proto unifikujeteTF = fun(TP, TV)
, čímž se magicky zjistí výsledná hodnotaTV
, kterou vrátíte.
- Rekurzivně se zavoláte na výraz
Pro příklad odvodíme typ \a -> \b -> b a
: (zanoření seznamu odpovídá zanoření rekurze)
- Nejvrchnější výraz je
lambda('a', Vyraz)
, do kontextu přídáme, že'a'
má typX1
a pokračujeme rekurzivně- Další výraz je
lambda('b', Vyraz)
, do kontextu přídáme, že'b'
má typX2
a pokračujeme rekurzivně- Další výraz je
app(V1, V2)
, začneme nejdřív vyhodnnocovatV1
:V1
je'b'
, to podle kontextu má typX2
, takžeV1
má typX2
- pokračuju pro
V2
V2
je'a'
, to podle kontextu má typX1
, takžeV2
má typX1
- do pravidla
TF=fun(TP,TV)
dosadíme a dostanemeX2=fun(X1, V)
. Prologová unifikace zařídí, žeX2
se všude nahradí za funkci zX1
doV
. Výsledný typ aplikace jeV
.
- Další výraz je
- Vnitřek vnitřnější lambdy má typ
V
a parametr má typX2
, celá lambda má tedy typfun(X2, V)
, což je kvůli unifikacifun(fun(X1,V),V)
. Záznam pro ‘b’ odebereme z kontextu.
- Další výraz je
- Vnitřek vnější lambdy má typ
fun(fun(X1,V),V)
a parametr má typX1
, takže celý výraz má typfun(X1, fun(fun(X1,V), V))
. Záznam pro ‘a’ odebereme z kontextu.
Pokud si výsledek přepíšete zpátky do běžné šipkovité notace, vyjde vám X1 -> (X1 -> V) -> V
, což mimochodem (až na jména proměnných) odpovídá tomu, co si o tom samém výrazu myslí Haskell:
ghci> :t \a -> \b -> b a \a -> \b -> b a :: t1 -> (t1 -> t2) -> t2
O systému si kdyžtak můžete víc přečíst tady.
Úkol, část 2
Vyrobte predikát lambda_typ/2
, který implementuje popsané odvozování typu z rozparsovaného výrazu. Pro kontrolu odvoďte typ \f -> \g -> \x -> g(f(g(f(g x))))
.
Disclaimer
Pokud pro parsování rozumně použijete gramatiky, řešení vyjde zhruba na 20 neúplně obsazených řádků Prologu.