Leniwie czy gorliwie?

14 Maja 2019

Co to znaczy, że język programowania jest leniwy? Jakie języki w ogóle mogą być leniwe? Poniżej odpowiem na te pytania, a także zrobię szybkie podsumowanie poprzedniego miesiąca.

Ostatnio nie miałem czasu pisać postów i de facto mój jedyny post w kwietniu, poza podsumowaniem marca, to było satyryczne porównanie problemu P = NP i czy Bóg istnieje. Co w tym kwietniu się działo? Byłem wolontariuszem na konferencji Scalar (prawdę mówiąc, nie ciągnie mnie do Scali), potem mieliśmy turniej - drugą dywizję EQC (Europejski Puchar Quidditcha) w Warszawie, gdzie byłem sędzią i pomagałem w organizacji. Potem były święta, a w ostatni weekend pojechałem do Poznania na Pyrkon.

W między czasie zacząłem robić research do mojej pracy magisterskiej, która idzie w kierunku jakiegoś leniwego języka na platformę .NET, a także rozpocząłem przygodę z programem Coq, który pomaga w dowodzeniu twierdzeń przy pomocy programów funkcyjnych.

Imperatywny świat

Jeśli spojrzymy na model obliczeniowy naszego komputera, to jest to imperatywna maszyna. Mamy polecenia, wykonywane przez procesor, które modyfikują pamięć. Kolejność wykonania instrukcji jest ważna, żeby algorytm działał poprawnie. Oznacza to, że każde wyrażenie musi być obliczone od razu jak tylko je zobaczymy. W szczególności jeśli wołamy funkcję z parametrem, z którego ona nie korzysta, to i tak musimy jego wartość obliczyć.

To nazywamy gorliwością lub semantyką strict.

Program w języku funkcyjnym jako graf

W przypadku czystych języków funkcyjnych mamy znacznie więcej wolności jeśli chodzi o kolejność obliczeń. Brak skutków ubocznych oznacza, że nie musimy traktować programu jako listy instrukcji, możemy za to użyć struktury grafowej do wyrażania obliczenia.

Popatrzmy na przykład takiej aplikacji

let square x = x * x
in square (2 + 2)

             |app|
      |square|   |app|
              |app| |2|
             |+| |2|

Mamy ładne drzewko aplikacji. Stanie się ono grafem, gdy zaczniemy dokonywać redukcji (obliczania), albowiem jeśli dane poddrzewo jest używane kilkakrotnie w ciele funkcji, to nie będzie kopiowane.

Obliczenie programu to redukcja grafu

Spotkamy się z różnymi algorytmami na obliczanie wyrażenia przedstawionego za pomocą grafu, ale wszystkie opierają się w dużej mierze na idei β-redukcji.

Jeśli mamy funkcję w postaci lambda abstrakcji \x -> e, i aplikację tej funkcji do argumentu y, to podczas β-redukcji uzyskamy wyrażenie e', takie że wszystkie wystąpienia x zostały zastąpione przez wyrażenie y.

(\x -> x * x)(2+2)
----β redukcja----
   (2+2) * (2+2)

W tym momencie użyjemy redukcji dla funkcji wbudowanych i dostaniemy wynik 16.

Własności leniwej redukcji

Podstawową ideą leniwości jest obliczanie wyrażeń tak późno jak to możliwe. Co oznacza, że w momencie aplikacji nie obliczamy parametrów. Dopiero aplikacja funkcji strict takich jak (+), (-) itp. oraz wyrażenia case..of wymuszają obliczenie wartości wyrażenia.

Np. w let const x y = x in const 1 (duże obliczenie) od razu dostaniemy 1 i duże obliczenie nie będzie dotykane.

Druga idea leniwości to współdzielenie, o którym wspomniałem przy określaniu grafu. Ponieważ 2+2 może być współdzielonym wierzchołkiem, to w momencie gdy w jednym miejscu będzie potrzebne do obliczeń, to przekształci się na 4 i we wszystkich innych miejscach nie trzeba będzie ponawiać obliczenia.

Co ciekawe, w definicji języka Haskell jest napisane, że jest on tylko non-strict (obliczanie jak najpóźniej), natomiast w praktyce kompilator GHC zapewnia pełną leniwość.

Benefity

Dużą korzyścią jest to, że na efektywnie działającej maszynie redukującej grafy, nasz program będzie śmigał, bo stara się nie wykonywać tej samej pracy wiele razy, a wykona ją tylko jeśli będzie niezbędna.

Możemy korzystać z nieskończonych struktur danych, co pozwala nam na nieco inne myślenie o obliczeniach.

Możemy zdefiniować sobie polecenie takie jak print 4 i przekazywać do funkcji bez jego wywołania.

Jest to bardzo ciekawy koncept, choć nie najprostszy do przyswojenia. Mi zajęło trochę czasu (tak ze 3 tygodnie) zanim zacząłem rozumieć leniwość - przestała mi przeszkadzać, bo program działał inaczej niż byłem przyzwyczajony. Minęło trochę więcej zanim nauczyłem się jej używać, aby korzystać z jej dobroci.