Dlaczego używamy trwałych struktur danych w programowaniu funkcjonalnym?

Programowanie funkcjonalne wykorzystuje trwałe struktury danych i niezmienne obiekty. Moje pytanie brzmi: dlaczego tak ważne jest posiadanie takich struktur danych? Chcę na niskim poziomie zrozumieć, co by się stało, gdyby struktura danych nie była trwała? Czy program często się zawieszał?

Podczas pracy z niezmiennymi obiektami danych funkcje mają tę właściwość, że za każdym razem, gdy wywołuje się je przy użyciu tych samych danych wejściowych, generują te same dane wyjściowe. Ułatwia to konceptualizację obliczeń i ich poprawne. Ułatwia to także ich testowanie.

To dopiero początek. Ponieważ matematyka od dawna działa z funkcjami, istnieje wiele technik wnioskowania, które możemy wypożyczyć z matematyki i używać ich do rygorystycznego rozumowania programów. Najważniejszą zaletą z mojego punktu widzenia jest to, że systemy typów programów funkcjonalnych są dobrze rozwinięte. Jeśli więc gdzieś się pomylisz, istnieje duże prawdopodobieństwo, że pojawi się jako niedopasowanie typu. Tak więc pisane programy funkcjonalne są zwykle bardziej niezawodne niż programy imperatywne.

W przeciwieństwie do pracy ze zmiennymi obiektami danych, najpierw masz poznawcze obciążenie zapamiętywania i zarządzania wieloma stanami, przez które obiekt przechodzi podczas obliczeń. Musisz zadbać o to, aby robić rzeczy we właściwej kolejności, upewniając się, że wszystkie właściwości potrzebne do określonego kroku są w tym momencie spełnione. Łatwo jest popełniać błędy, a systemy typów nie są wystarczająco mocne, aby je uchwycić.

Matematyka nigdy nie działała ze zmiennymi obiektami danych. Nie ma więc żadnych technik rozumowania, które moglibyśmy od nich pożyczyć. Istnieje wiele własnych technik opracowanych w dziedzinie informatyki, zwłaszcza Logika Floyda-Hoare'a . Są one jednak trudniejsze do opanowania niż standardowe techniki matematyczne, większość uczniów nie może sobie z nimi poradzić, dlatego rzadko się uczą.

Aby uzyskać szybki przegląd różnic między tymi dwoma paradygmatami, możesz zapoznać się z kilkoma pierwszymi materiałami z moich notatek z wykładów na temat zasad języków programowania .

Jest to łatwiejsze do prawidłowego pracy ze strukturami trwałe danych, niż jest do pracy z modyfikowalnych struktur danych. Powiedziałbym, że jest to główna zaleta.

Oczywiście teoretycznie wszystko, co robimy z trwałymi strukturami danych, możemy również robić ze zmiennymi strukturami i odwrotnie. W wielu przypadkach trwałe struktury danych generują dodatkowe koszty, zwykle dlatego, że ich część musi zostać skopiowana. Te względy sprawiłyby, że trwałe struktury danych byłyby znacznie mniej atrakcyjne 30 lat temu, gdy superkomputery miały mniej pamięci niż twój telefon komórkowy. Ale obecnie głównymi przeszkodami w produkcji oprogramowania wydają się być czas programowania i koszty utrzymania. Dlatego jesteśmy gotowi poświęcić pewną wydajność w wykonywaniu dla wydajności w rozwoju.

Dlaczego korzystanie z trwałych struktur danych jest łatwiejsze? Ponieważ ludzie naprawdę źle śledzą aliasing i inne rodzaje nieoczekiwanych interakcji między różnymi częściami programu. Są one automatycznie myśleć, że ponieważ dwie rzeczy są nazywane xi y, a następnie mają nic commmon. Po wszystkim trzeba się domyślić, że „gwiazda poranna” i „gwiazda wieczorna” to tak naprawdę to samo. Podobnie bardzo łatwo jest zapomnieć, że struktura danych może ulec zmianie, ponieważ inne wątki z nią pracują, lub dlatego, że nazwaliśmy metodę, która zdarza się zmieniać strukturę danych itp. Wiele z tych problemów po prostu nie występuje, gdy pracujemy z trwałe struktury danych.

Trwałe struktury danych mają również inne zalety techniczne. Zazwyczaj łatwiej jest je zoptymalizować. Na przykład zawsze możesz swobodnie skopiować trwałą strukturę danych do innego węzła w chmurze, jeśli chcesz, nie ma obaw o synchronizację.

Dodając do odpowiedzi innych i wzmacniając podejście matematyczne, programowanie funkcjonalne ma również niezłą synergię z relacyjną algebrą i połączeniami Galois.

Jest to niezwykle przydatne w obszarze metod formalnych.
Na przykład:

• Formalne dowody weryfikacji programu są uproszczone dzięki rozszerzonej kontroli statycznej;
• Szereg właściwości Algebry relacyjnej jest przydatny w rozwiązywaniu SAT, z narzędziami takimi jak Alloy;
• Galois Connections pozwala na obliczeniowe podejście do specyfikacji oprogramowania, jak widać na tym blogu , w odniesieniu do artykułu Shin-Cheng Mu i José Nuno Oliveira.
• Połączenia Galois (i programowanie funkcjonalne) mogą być używane w stylu Design by Contract, ponieważ są one bardziej ogólną koncepcją niż Hoare Logic.

Przykład

$\{p\} P \{q\}$$[P] \cdot \phi_p \subseteq \phi_q \cdot [P]$

• $[P]$$P$
• $\phi_p$$\phi_q)$$p$$q$

Takie podejście pozwala również na najsłabsze obliczenia wstępne i najsilniejsze obliczenia wstępne , co przydaje się w wielu sytuacjach.

Chcę zrozumieć na niskim poziomie, co by się stało, gdyby struktura danych nie była trwała?

Spójrzmy na generator liczb pseudolosowych z ogromną przestrzenią stanów (jak „ twister Mersenne ” o stanie 2450 bajtów) jako strukturę danych. Tak naprawdę nie chcemy używać żadnej liczby losowej więcej niż jeden raz, więc wydaje się, że nie ma powodu, aby wdrażać ją jako niezmienną trwałą strukturę danych. Teraz zadajmy sobie pytanie, co może pójść nie tak w następującym kodzie:

mt_gen = CreateMersenneTwisterPRNGen(seed)
integral = MonteCarloIntegral_Bulk(mt_gen) + MonteCarloIntegral_Boundary(mt_gen)

Większość języków programowania nie określa kolejności MonteCarloIntegral_Bulki MonteCarloIntegral_Boundarybędzie oceniana. Jeśli oba przyjmą jako argument odwołanie do mutowalnego mt_gen, wynik tego obliczenia może zależeć od platformy. Co gorsza, mogą istnieć platformy, na których wynik nie jest w ogóle odtwarzalny pomiędzy różnymi przebiegami.

Można zaprojektować wydajną, zmienną strukturę danych dla mt_gen, tak aby każde przeplatanie wykonania MonteCarloIntegral_Bulki MonteCarloIntegral_Boundarydawało „poprawny” wynik, ale inne przeplatanie generalnie prowadzi do innego „poprawnego” wyniku. Ta nieodtwarzalność powoduje, że odpowiednia funkcja jest „nieczysta”, a także prowadzi do innych problemów.

Niereprodukowalności można uniknąć poprzez wymuszenie stałej kolejności wykonywania sekwencyjnego. Ale w takim przypadku kod może być ustawiony w taki sposób, aby w danym momencie było dostępne tylko jedno odwołanie do mt_gen. W typowym funkcjonalnym języku programowania można zastosować typy unikatowości, aby wymusić to ograniczenie, umożliwiając w ten sposób bezpieczne modyfikowalne aktualizacje również w kontekście czysto funkcjonalnych języków programowania. Wszystko to może brzmieć ładnie i elegancko, ale przynajmniej teoretycznie symulacje Monte Carlo są żenująco równoległe, a nasze „rozwiązanie” właśnie zniszczyło tę właściwość. To nie jest tylko problem teoretyczny, ale bardzo realny problem praktyczny. Musimy jednak zmodyfikować (oferowaną przez nas funkcję) nasz generator liczb pseudolosowych i sekwencję liczb losowych, które produkuje, i żaden język programowania nie może zrobić tego automatycznie dla nas. (Oczywiście możemy użyć innej biblioteki liczb pseudolosowych, która już oferuje wymaganą funkcjonalność).

Na niskim poziomie, zmienne struktury danych łatwo prowadzą do braku powtarzalności (a zatem i zanieczyszczenia), jeśli kolejność wykonywania nie jest sekwencyjna i ustalona. Typową strategią konieczną do rozwiązania tych problemów jest sekwencyjne fazy ze stałą kolejnością wykonywania, podczas których zmieniane są zmienne struktury danych, oraz równoległe fazy z dowolną kolejnością wykonywania, podczas których wszystkie współużytkowane zmienne struktury danych pozostają stałe.

Andrej Bauer podniósł kwestię aliasingu dla zmiennych struktur danych. Co ciekawe, różne imperatywne języki, takie jak Fortran i C, mają różne założenia dotyczące dozwolonego aliasingu argumentów funkcji, a większość programistów jest zupełnie nieświadoma, że ​​ich język ma w ogóle model aliasingu.

Niezmienność i semantyka wartości mogą być nieco przereklamowane. Co ważniejsze, system typów i struktura logiczna (jak abstrakcyjny model maszyny, model aliasingu, model współbieżności lub model zarządzania pamięcią) twojego języka programowania zapewniają wystarczające wsparcie dla „bezpiecznej” pracy z „wydajnymi” danymi Struktury. Wprowadzenie „semantyki ruchu” do C ++ 11 może wyglądać jak ogromny krok wstecz pod względem czystości i „bezpieczeństwa” z teoretycznego punktu widzenia, ale w praktyce jest odwrotnie. System typów i logiczna struktura języka zostały rozszerzone, aby usunąć ogromne części niebezpieczeństwa związanego z nową semantyką. (I nawet jeśli pozostaną ostre krawędzie, nie oznacza to, że nie można tego poprawić „lepszym”

Uday Reddy podniósł kwestię, że matematyka nigdy nie działała ze zmiennymi obiektami danych oraz że systemy typów programów funkcjonalnych są dobrze opracowane dla niezmiennych obiektów danych. Przypomniało mi to wyjaśnienie Jean-Yvesa Girarda, że ​​matematyka nie jest wykorzystywana do pracy ze zmiennymi obiektami, kiedy próbuje motywować logikę liniową.

Można zapytać, jak rozszerzyć system typów i strukturę logiczną funkcjonalnych języków programowania, aby umożliwić „bezpieczną” pracę z „wydajnymi”, zmiennymi, nietrwałymi strukturami danych. Jednym z problemów może być to, że klasyczne logiki i algebry logiczne mogą nie być najlepszym logicznym szkieletem do pracy ze zmiennymi strukturami danych. Być może logika liniowa i monoidy przemienne mogą być lepiej dostosowane do tego zadania? Być może powinienem przeczytać, co Philip Wadler ma do powiedzenia na temat logiki liniowej jako systemu pisma dla funkcjonalnych języków programowania? Ale nawet jeśli logika liniowa nie byłaby w stanie rozwiązać tego problemu, nie oznacza to, że system typów i struktura logiczna funkcjonalnego języka programowania nie mogą zostać rozszerzone, aby umożliwić „bezpieczne” i „wydajne”