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 do b 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 typ T
- celá lambda má následně typ funkce z X (protože to je typ parametru) do T (protože to je typ výsledku), tedy fun(X,T).
Pokud ohodnocujete typ aplikace app(Funkce,Parametr), pak:
- Rekurzivně se zavoláte na výraz Funkce, vyjde vám typ funkce TF
- Rekurzivně se zavoláte na výraz Parametr, vyjde vám typ parametru TP
- Víte, že funkce typu TF přijala parametr typu TP a musí vrátit nějaký typ výsledku TV. Proto unifikujete TF = fun(TP, TV), čímž se magicky zjistí výsledná hodnota TV, kterou vrátíte.

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á typ X1 a pokračujeme rekurzivně
- Další výraz je lambda('b', Vyraz), do kontextu přídáme, že 'b' má typ X2 a pokračujeme rekurzivně
  - Další výraz je app(V1, V2), začneme nejdřív vyhodnnocovat V1:
    - V1 je 'b', to podle kontextu má typ X2, takže V1 má typ X2
  - pokračuju pro V2
    - V2 je 'a', to podle kontextu má typ X1, takže V2 má typ X1
  - do pravidla TF=fun(TP,TV) dosadíme a dostaneme X2=fun(X1, V). Prologová unifikace zařídí, že X2 se všude nahradí za funkci z X1 do V. Výsledný typ aplikace je V.
- Vnitřek vnitřnější lambdy má typ V a parametr má typ X2, celá lambda má tedy typ fun(X2, V), což je kvůli unifikaci fun(fun(X1,V),V). Záznam pro ‘b’ odebereme z kontextu.
Vnitřek vnější lambdy má typ fun(fun(X1,V),V) a parametr má typ X1, takže celý výraz má typ fun(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.