Program jako funkcja całkowita - czyli kiedy naprawdę nie ma błędów

pawelwlodarski.blogspot.com 8 lat temu

"Litr czystej poproszę" - to zdanie wypowiedziane w całodobowym sklepie branżowym niesie ze sobą wystarczająca ilość informacji aby było wiadomo "o co chodzi". A wiadomo o co chodzi gdyż kontekst już definiuje pewne pojęcia jak to, iż chodzi o napój w tym sklepie, iż ma się to odbyć teraz i iż popłynie hajs. Te rzeczy są oczywiste.

Wynik 2+2=4 także jest oczywisty. jeżeli zapytamy o rezultat porównania 2 + 2 == 4 to czytelnik o ponadprzeciętnej podejrzliwości może szukać podstępu w definicji operatora + (tak, w niektórych językach można go zdefiniować jak się chce) albo widzi spisek w tym jak operator == porównuje wartości, a może jest tu jakiś "Boxing" a może porównuje referencje? Raczej mało komu przyjdzie do głowy, iż może mechanika działa prawidłowo ale 2+2 to wcale nie 4? eeee ... iż co? Brzmi to z pozoru absurdalnie ale jednak są ludzie, którym oczywistość nie wystarcza i wyprowadzili wcale niebanalny dowód iż 2+2 to faktycznie 4

Teraz inna sytuacja - słyszysz zdanie : "W moim programie jest Błąd" a jeżeli ma być światowo to "W moim programie jest Bug" i zwykle rzeczą, na której koncentruje się sytuacja jest ten Bug. Raczej nie usłyszysz w odpowiedzi "W twoim programie jest Bug, a jak zdefiniowałeś pojęcie programu?" albo "zdefiniuj warunki wymagane do stwierdzenia jest Błąd" czy wyjątek to błąd , czy sam fakt, iż może polecieć wyjątek ale nie poleciał to błąd? Czy jeżeli nie leci wyjątek a jest zły rezultat to jest to błąd? No i w końcu czy jeżeli wszystko działa to w programie jest błąd czy go nie ma?

Po tym dowodzie na dwie strony, iż 2+2=4 ostatnie zdanie nie powinno być takie oczywiste - Czy jeżeli program działa i zwraca poprawny wynik to jest w nim błąd?.Zagłębmy się w ten interesujący problem i zdefiniujmy "Program" i "Błąd".

Korzenie

Powyższy obrazek jest skopiowany ze strony na wikipedii : Human Computer. Bo oto okazuje się, iż komputery istniały jeszcze zanim powstały ...komputery.

The term "computer", in use from the early 17th century (the first known written reference dates from 1613), meant "one who computes": a person performing mathematical calculations, before electronic computers became commercially available.

Ha! Czyli nie dość, iż trzeba zdefiniować co to jest program to jeszcze nie jest jasne co to jets ten "komputer". I teraz sformułowanie "Babcia kupiła mi na komunie komputer" może choćby zakończyć się sprawą w sądzie na skutek uprawiania niezgodnego z prawem niewolnictwa!

Ciekawy jest fragment o tym co oni robili "a person performing mathematical calculations". Pewnie nie jeden profesorek rzuci teraz we mnie cyrklem ale teoretycznie coś takiego :


fun czyProstokątny(a:Integer,b:Integer,c:Integer):Boolean = pow(a,2)+pow(b,2) == pow(c,2)

to też jest jakieś tam "mathematical calculations" i przy założeniu, iż "a" i "b" to przyprostokątne a "c" to zawsze przeciwprostokątna to ta funkcja sprawdza czy trójkąt jest prostokątny. Ale czy sprawdza? Tego nie wiadomo. Bo co robi funkcja "pow"? Być może wydaje z głośnika na płycie głównej dźwięki "POWPOW" ?

Przydałoby się tutaj jakieś twierdzenie w stylu Dla każdego x należącego do zbioru liczb całkowitych pow(x,2)=x * x . Oczywiście można tak jechać dalej ze znaczkiem "*" ale tutaj założymy, iż to mnożenie, które działa "dobrze" bez wnikania w definicję "dobrze" bo to jest tylko wstep do ciekawszych rzeczy.

Czy coś może pójść nie tak?

Wydaje się, iż pierwszym problemem może być przekroczenie zakresu Integera. Jaki jest zakres Integera ? "Ja wiem!Ja wiem! W javadocu jest , iż 2 31 - 1"

I to jest właśnie takie myślenie językiem programowania. Czasem niestety jednocześnie pierwszym i jedynym jaki dana osoba napotka w życiu. No bo zobacz - taki Haskell wydaje się mieć trochę na zakresy wyjebane :

Dowód na czytanie z pliku?

Ciekawie zaczyna się robić kiedy zaczniemy drążyć "skąd dokładnie brane jest a,b i c"? Niechże to będzie plik CSV z jedną linią by było prościej

3,4,5
I teraz np mamy dwie dodatkowe funkcje
fun czytaj(plik:File):String
fun parsuj(linia:String):(a:Integer,b:Integer,c:Integer)
Ba i choćby teraz można zrobić kompozycję bezpośrednio z pliku w wynik sprawdzania czy trójkąt jest prostokątny
czytaj andThen parsuj andThen czyProstokątny

- Łooołooołooołoo łooooo chwila chwila chwillllla a co jak się wyjebie?"
- ale co?
- no to czytanie z pliku?
- ale ... ale jak?
- no jak pliku nie będzie?
- no.. no.. to może załóżmy, iż zawsze jest...

Wydaje mi się, iż powyższy problem jest przedstawiony bardziej fachowo (i bez słowa "wyjebie" które może zgorszyć niejednego przedstawiciela zblazowanej klasy średniej) w poniższym abstrakcie.

Otóż takie teoretyczne rozważania rypią się gdy mamy do czynienia z czymś co dosyć trudno przedstawić "matematycznie" jak na przykład czytanie z bazy czy przesyłanie danych po sieci - no bo jak , no jak wygląda teoretycznie poprawna funkcja "zaciągnijLegalnieFilmZTorrenta". No i dopiero wyjście z tej sytuacji znalazł Eugenio Moggi a smaczku dodaje, iż abstrakt pochodzi z jego pracy zatytułowanej Notions of computation and monads (moooooooooooooooonads!!!)

Definicja BUGa jako funkcji

Tak dla przypomnienia - funkcja całkowita to na przykład dodawanie bo co byśmy tam nie podali to i tak zadziała. Funkcja częściowa to dzielenie bo dla argumentu gdzie dzielimy przez zero nie jest ona określona. jeżeli zastosujemy dzielenie z założeniem, ze zadziała dla każdej liczby - wtedy mamy błąd.

funkcja FormularzRejestracyjny=>User jest określona dla wszystkich poprawnie wypełnionego formularza ale nieokreślona dla Formularza, który w polu wiek ma wartość "DaaaajKamienia"

funkcja Plik=>String jest określona jedynie dla zbioru poprawnie zdefiniowanych i plików.

funkcja IdZamowienia=>Zamowienie jest określona jedynie dla istniejących zamówień.

funkcja OdpytanieZewnętrznegoAPI => Wynik też jest częściowa bo określona tylko dla sytuacji kiedy otrzymamy jakiś wynik.

Nie wiem czy ktoś z was podchodizł do tego od tej strony - ja kiedyś nie. zwykle po prostu chodziło o obsługę wyjątków. Tymczasem na obsługę wyjątków można trochę tak patrzeć jak na taki zewnętrzny hak, który umożliwia nam używanie funkcji częściowych tak jakby one były całkowite. Czyli poza standardowym znaczeniem BUGa kiedy to funkcja zwraca po prostu zły wynik (f(a,b)=a+b+1 - funkcja czysta ale zjebana) dochodzi dodatkowy rodzaj Błędu.

Błąd - sytuacja w której, funkcja częściowa jest używana tak jakby była całkowita. Np takie coś

 sprawdzLinie:String=>Boolean = parsujLinie and Then czyProstokątny
można zdefiniować jako błąd gdyż funkcja parsujLinie w kontekście naszego przykładu jest zdefiniowana jedynie dla takiej formy gdzie w linii jesta,b,c i to choćby może przejść wszystkie testy i chodzić na produkcji 5 lat. Cały czas kwalifikuje się to jako błąd.

Jak sprawdzić czy funkcja jest całkowita? - scalacheck.

Wizualizacja funkcji częściowej. Czerwona Kulka może symbolizować zapytanie do bazy danych, które zakończyło się niepowodzeniem.

Kompozycje i efekty

Cały problem z wyjątkami polega na tym, iż przeszkadzają one w kompozycji a kompozycja to "Reusage (Rejusedż)" czyli święta gral programowania. No bo jak mam funkcję String=>(Int,Int,Int), która mówi mi, iż zwraca trzy elementowego Tupla (z polskeigo krotkę) a tak naprawde zwraca tego Tupla albo ch.. wie jaki wyjątek to ja nie moge sobie prosto tej funkcji skomponować z (Int,Int,Int) => Boolean bo na wejściu wcale nie muszą pojawić się trzy inty!!!

No dobra ponarzekalimy ale gdzie jest SOLUSZYN? Zamiast udawać, iż funkcja częściowa to funkcja całkowita i try-catchem łapać pokemony może da rade zamienić jakoś te funkcję częściową w całkowitą? I to zaproponował właśnie Eugenio Moggi - chyba to zaproponował bo połowy jego pracy nie rozumiem ale poznaje rysunki, podobne do tych które są na stronie wiki o monadach (te takie ze strzałkami).

Klasycznie jest coś takiego :

val divide:(Int,Int)=>Int = (a,b) => a/b

try{
    divide(4,0)
}catch{
    case e:ArithmeticException => println("Kalwi & Remi - EXPLOSION")
}
I naprawdę ważne jest aby zrozumieć, iż tutaj to try, jest takim zewnętrznym klejem który utrudnia kompozycję.

Dalej mamy dedykowany typ dla funkcji częściowej:

val partialDivide : PartialFunction[(Int,Int),Int] = {
    case (a,b) if b!=0 => a/b
}

println(partialDivide.isDefinedAt(4,0))  //false
Tutaj już plus jest taki, iż nie udajemy, iż każdy argument ma jakiś wynik.

I teraz następuje zamiana funkcji częściowej na całkowitą

val totalDivide: ((Int, Int)) => Option[Int] =partialDivide.lift

println(totalDivide(4,0))  //None
println(totalDivide(4,2))  //Some(2)

"totalDivide" jest funkcją całkowitą i dla wszystkich argumentu zwraca ona rezultat. Tam gdzie dzielenie ma sens będzie to Some tam gdzie nie ma będzie None ale będzie! Może powstać pytanie ale co z tego jak w wyniku dostajemy jakiś "twór"? Ów twór jest tzw. Typem wyższego rzędu (po javowemu "klasa z generykiem") i obsługuje się go przy pomocy funkcji wyższego rzędu oraz pattern matchingu. Drugiego mechanizmu w Javie nie ma a pierwszy jest od niedawna dlatego w półswiatku javowym owe podejście może wydawać się bardzo egzotyczne.

Co z kompozycją? Jest cała teoria opisująca jak to się komponuje i ze zwykłymi funkcjami jak i z innymi tworami. Jedno popularne nazewnictwo używa na twory słów Funktor, Monada itd ale też spotkałem się z podejściem do tego jako do Efektu i np. Option to Efekt braku czegoś a Future Efekt czasu w obliczeniach.

Owy efekt spełnia pewne prawa i aby się przekonać, iż na pewno je spełnia możemy użyć scalacheck. Ba! ScalaZ ma choćby gotowy zestaw testów Scalachecka by sprawdzić czy aby na pewno wiemy z czym mamy do czynienia : Functor Laws

No i jak nasz efekt spełnia prawa Funktora to możemy śmiało pisać z założeniem, Option(x).map(f).map(g) to to samo co Option(x).map(f andThen g)

Tyle w temacie

Celem tego wpisu nie jest brnięcie dalej ale własnie zatrzymanie się w tym miejscu. Temat jest jak rzeka a za węgłem czekają Funktory,Monady, Monoidy, Foldable,Kleisli, Transformatory Monad czy inne potężne narzędzia kompozycji efektów. zwykle na co dzień nie mamy czasu/ochoty zatrzymać się na chwilę i poddać kontemplacji nad tym co my adekwatnie robimy. Jednak należy pamiętać, iż nasze obecne wnioski budowane są na dogmatycznych założeniach - jeżeli czasem im się bliżej nie przyjrzymy to wiele ciekawych dróg i perspektyw może być dla nas na zawsze zamkniętych :(

Anegdota o .Necie

Zazwyczaj na początku nauki instaluje się jakiś kompilator , pisze hello world i dalej jakieś tam proste przykłady. Ponieważ bez ogólnych podstaw teoretycznych mechanizmy konkretnego języka staną się jedynymi ilustracjami tychże mechanizmów to istnieje niebezpieczeństwo, iż ludzie zaczną utożsamiać implementacje z koncepcjami. W javie to będzie na przykład "polimorfizm - aha czyli dziedziczenie klas" albo powtarzanie bez głębszego zastanowienia, iż wszystkie pola w klasie (bo przecież nie może być poza klasą nie?) muszą być private bo..bo.. bo enkapsulacja i ch*j.

No i raz było w Łodzi spotkanie grupy devs@lodz, która wykształciła się z grupy dot netowej. No i jest to spotkanie i gostek gada o MVC ale tak gada jakby używał cały czas słowa samochód ale chodziło mu o jedynie o Poloneza. Od słowa do słowa zrozumiałem, iż Microsoft im tam potworzył po jednej implementacji wszystkiego i MVC to po prostu nazwa frameworka i też w moim odczuciu, trochę zdziwili się, iż jak w Javie chcesz mieć MVC to myślisz o koncepcji i wybierasz sobie dopiero jedno z narzędzi, które to realizuje.

Innym analogicznym przykładem rozmowa o systemie operacyjnym gdy znasz tylko windowsa - "dobra znajomość systemu operacyjnego wymaga płynnej obsługi menu start" - czy coś w tym stylu.

Studiowanie to gorący temat w IT zwłaszcza, iż w jakimś tam rankingu ostatnio dwie polskie uczelnie były w 5 setce a żadna Łódzka się choćby nie załapała ale polecam pogrzebać na edx czy courserze i można znaleźć naprawdę interesujące kursy online dostarczane przez uczelnie z samej czołówki. Do tego wiele z tych uczelni ma swoje własne portale jak http://ocw.mit.edu/index.htm



Idź do oryginalnego materiału