Jak w programowaniu funkcjonalnym osiąga się modułowość dzięki prawom matematyki?

Czytam w tym pytaniu, że programiści funkcjonalni używają matematycznych dowodów, aby upewnić się, że ich program działa poprawnie. Brzmi to o wiele łatwiej i szybciej niż testy jednostkowe, ale pochodzące z tła OOP / testów jednostkowych Nigdy tego nie widziałem.

Czy możesz mi to wyjaśnić i podać przykład?

Dowód jest znacznie trudniejszy w świecie OOP ze względu na skutki uboczne, nieograniczone dziedziczenie i nullbycie członkiem każdego rodzaju. Większość dowodów opiera się na zasadzie indukcji, aby pokazać, że wykorzystałeś wszystkie możliwości, a wszystkie 3 z tych rzeczy utrudniają udowodnienie.

Powiedzmy, że wdrażamy drzewa binarne, które zawierają wartości całkowite (dla uproszczenia składni nie będę wprowadzał do tego programowania ogólnego, chociaż nic by to nie zmieniło). W Standardowym ML zdefiniowałbym to jako to:

datatype tree = Empty | Node of (tree * int * tree)

Wprowadza to nowy typ o nazwie, treektórego wartości mogą występować w dokładnie dwóch odmianach (lub klasach, których nie należy mylić z koncepcją OOP klasy) - Emptywartość, która nie przenosi żadnych informacji, oraz Nodewartości, które niosą 3-krotkę, której pierwsza i ostatnia elementy to trees, a środkowym elementem jest int. Najbliższe zbliżenie do tej deklaracji w OOP wyglądałoby tak:

public class Tree {
    private Tree() {} // Prevent external subclassing

    public static final class Empty extends Tree {}

    public static final class Node extends Tree {
        public final Tree leftChild;
        public final int value;
        public final Tree rightChild;

        public Node(Tree leftChild, int value, Tree rightChild) {
            this.leftChild = leftChild;
            this.value = value;
            this.rightChild = rightChild;
        }
    }
}

Z zastrzeżeniem, że zmienne typu Drzewo nigdy nie mogą być null.

Napiszmy teraz funkcję do obliczenia wysokości (lub głębokości) drzewa i załóżmy, że mamy dostęp do maxfunkcji, która zwraca większą z dwóch liczb:

fun height(Empty) =
        0
 |  height(Node (leftChild, value, rightChild)) =
        1 + max( height(leftChild), height(rightChild) )

Zdefiniowaliśmy heightfunkcję według przypadków - istnieje jedna definicja dla Emptydrzew i jedna definicja dla Nodedrzew. Kompilator wie, ile istnieje klas drzew i wyda ostrzeżenie, jeśli nie zdefiniujesz obu przypadków. Wyrażenie Node (leftChild, value, rightChild)w podpisie funkcji wiąże wartości 3-krotki do zmiennych leftChild, valueoraz rightChildodpowiednio więc możemy odnieść się do nich w definicji funkcji. Jest to podobne do zadeklarowania takich zmiennych lokalnych w języku OOP:

Tree leftChild = tuple.getFirst();
int value = tuple.getSecond();
Tree rightChild = tuple.getThird();

Jak możemy udowodnić, że heightpoprawnie wdrożyliśmy ? Możemy użyć indukcji strukturalnej , która składa się z: 1. Udowodnij, że heightjest poprawna w przypadku (przypadkach) bazowych naszego treetypu ( Empty) 2. Zakładając, że wywołania rekurencyjne heightsą poprawne, udowodnij, że heightjest to poprawne w przypadku przypadku nie będącego podstawą ) (gdy drzewo to tak naprawdę Node).

W kroku 1 widzimy, że funkcja zawsze zwraca 0, gdy argumentem jest Emptydrzewo. Jest to prawidłowe z definicji wysokości drzewa.

W kroku 2 funkcja powraca 1 + max( height(leftChild), height(rightChild) ). Zakładając, że wywołania rekurencyjne naprawdę zwracają wzrost dzieci, możemy zauważyć, że jest to również poprawne.

I to stanowi dowód. Łączne kroki 1 i 2 wyczerpują wszystkie możliwości. Zauważ jednak, że nie mamy mutacji, żadnych zer i istnieją dokładnie dwie odmiany drzew. Po usunięciu tych trzech warunków dowód szybko staje się bardziej skomplikowany, jeśli nie niepraktyczny.

EDYCJA: Ponieważ ta odpowiedź osiągnęła szczyt, chciałbym dodać mniej trywialny przykład dowodu i nieco dokładniej objąć indukcję strukturalną. Powyżej udowodniliśmy, że jeśli heightzwraca , to zwracana wartość jest poprawna. Jednak nie udowodniliśmy, że zawsze zwraca wartość. Możemy również użyć indukcji strukturalnej, aby to udowodnić (lub dowolną inną właściwość). Ponownie, podczas kroku 2, możemy przyjąć, że wstrzymania własności wywołań rekurencyjnych są zachowane, o ile wszystkie wywołania rekurencyjne działają na bezpośrednim potomku drzewo.

Funkcja może nie zwrócić wartości w dwóch sytuacjach: jeśli zgłosi wyjątek i zapętli się na zawsze. Najpierw udowodnijmy, że jeśli nie zostaną zgłoszone żadne wyjątki, funkcja kończy się:

1. Wykazać, że (jeśli nie zostaną zgłoszone wyjątki) funkcja kończy się dla przypadków bazowych ( Empty). Ponieważ bezwarunkowo zwracamy 0, to kończy się.

2. Wykazać, że funkcja kończy się w przypadkach innych niż bazowe ( Node). Są trzy wywołania funkcji tutaj: +, max, i height. Wiemy o tym +i maxrozwiązujemy, ponieważ są one częścią standardowej biblioteki języka i są zdefiniowane w ten sposób. Jak wspomniano wcześniej, możemy założyć, że właściwość, którą próbujemy udowodnić, jest prawdziwa w przypadku wywołań rekurencyjnych, o ile działają one w bezpośrednich poddrzewach, więc również wezwania do heightzakończenia.

To kończy dowód. Pamiętaj, że nie można udowodnić zakończenia przy pomocy testu jednostkowego. Teraz pozostaje tylko pokazać, że heightnie rzuca wyjątków.

1. Udowodnij, że heightnie wyrzuca wyjątków na przypadek podstawowy ( Empty). Zwrócenie 0 nie może zgłosić wyjątku, więc skończyliśmy.
2. Udowodnij, że heightnie zgłasza wyjątku w przypadku innym niż bazowy ( Node). Załóżmy jeszcze raz, że wiemy +i maxnie rzucamy wyjątków. A indukcja strukturalna pozwala nam założyć, że wywołania rekurencyjne też nie rzucą (ponieważ działają na bezpośrednie dzieci drzewa). Ale czekaj! Ta funkcja jest rekurencyjna, ale nie rekurencyjna . Możemy zdmuchnąć stos! Nasz próbowany dowód odkrył błąd. Możemy to naprawić, zmieniając heightsię w rekurencyjny .

Mam nadzieję, że to pokazuje, że dowody nie muszą być przerażające ani skomplikowane. W rzeczywistości za każdym razem, gdy piszesz kod, nieformalnie konstruujesz dowód w swojej głowie (w przeciwnym razie nie byłbyś przekonany, że właśnie zaimplementowałeś tę funkcję). Unikając zerowej, niepotrzebnej mutacji i nieograniczonego dziedziczenia, możesz udowodnić, że twoja intuicja jest poprawić dość łatwo. Te ograniczenia nie są tak surowe, jak mogłoby się wydawać:

• null jest wadą językową i zlikwidowanie go jest bezwarunkowo dobre.
• Mutacja jest czasem nieunikniona i konieczna, ale jest potrzebna o wiele rzadziej, niż się wydaje - zwłaszcza gdy masz trwałe struktury danych.
• Jeśli chodzi o posiadanie skończonej liczby klas (w sensie funkcjonalnym) / podklas (w sensie OOP) w porównaniu z nieograniczoną liczbą z nich, to temat jest zbyt duży, by dać jedną odpowiedź . Wystarczy powiedzieć, że istnieje kompromis między projektem - sprawdzalność poprawności a elastyczność rozszerzenia.

1. O wiele łatwiej jest wnioskować o kodzie, gdy wszystko jest niezmienne . W rezultacie pętle są częściej zapisywane jako rekurencja. Zasadniczo łatwiej jest zweryfikować poprawność rozwiązania rekurencyjnego. Często takie rozwiązanie będzie również czytać bardzo podobnie do matematycznej definicji problemu.

   Jednak w większości przypadków motywacja do przeprowadzenia rzeczywistego formalnego dowodu poprawności jest niewielka. Dowody są trudne, zajmują dużo czasu (ludzie) i mają niski zwrot z inwestycji.

2. Niektóre języki funkcjonalne (zwłaszcza z rodziny ML) mają wyjątkowo wyraziste systemy typów, które mogą zapewnić o wiele bardziej kompletne gwarancje, że system typu C (ale niektóre pomysły, takie jak generyczne, stały się również powszechne w językach głównego nurtu). Gdy program przejdzie kontrolę typu, jest to rodzaj zautomatyzowanego dowodu. W niektórych przypadkach będzie w stanie wykryć niektóre błędy (np. Zapomnienie przypadku podstawowego w rekurencji lub zapomnienie obsługi niektórych przypadków w dopasowaniu wzorca).

   Z drugiej strony, systemy tego typu muszą być bardzo ograniczone, aby można było je rozstrzygać . W pewnym sensie uzyskujemy więc gwarancje statyczne, rezygnując z elastyczności - a te ograniczenia są powodem, dla którego istnieją skomplikowane prace akademickie w stylu „ monadycznego rozwiązania rozwiązanego problemu w Haskell ”.

   Lubię zarówno bardzo liberalne, jak i bardzo ograniczone języki i oba mają swoje trudności. Ale nie jest tak, że ktoś byłby „lepszy”, każdy jest po prostu wygodniejszy do innego rodzaju zadania.

Następnie należy zauważyć, że dowody i testy jednostkowe nie są zamienne. Oba pozwalają nam ustalić granice poprawności programu:

• Testowanie nakłada górną granicę na poprawność: jeśli test się nie powiedzie, program jest niepoprawny, jeśli żaden test się nie powiedzie, jesteśmy pewni, że program obsłuży testowane przypadki, ale nadal mogą występować nieodkryte błędy.

  int factorial(int n) {
    if (n <= 1) return 1;
    if (n == 2) return 2;
    if (n == 3) return 6;
    return -1;
  }
  
  assert(factorial(0) == 1);
  assert(factorial(1) == 1);
  assert(factorial(3) == 6);
  // oops, we forgot to test that it handles n > 3…
  

• Dowody określają dolną granicę poprawności: udowodnienie niektórych właściwości może być niemożliwe. Na przykład może być łatwo udowodnić, że funkcja zawsze zwraca liczbę (to właśnie robią systemy typów). Ale może nie być możliwe udowodnienie, że liczba będzie zawsze < 10.

  int factorial(int n) {
    return n;  // FIXME this is just a placeholder to make it compile
  }
  
  // type system says this will be OK…
  

Słowo ostrzeżenia może być tutaj:

Chociaż ogólnie jest prawdą, co piszą tutaj inni - krótko mówiąc, że zaawansowane systemy typu, niezmienność i przejrzystość referencyjna mają duży wpływ na poprawność - nie jest tak, że testowanie nie odbywa się w świecie funkcjonalnym. Wręcz przeciwnie !

Dzieje się tak, ponieważ mamy narzędzia takie jak Quickcheck, które generują przypadki testowe automatycznie i losowo. Podajesz jedynie prawa, których musi przestrzegać funkcja, a następnie szybkie sprawdzenie sprawdzi te prawa pod kątem setek przypadkowych przypadków testowych.

Widzisz, jest to nieco wyższy poziom niż trywialne kontrole równości w kilku przypadkach testowych.

Oto przykład z implementacji drzewa AVL:

--- A generator for arbitrary Trees with integer keys and string values
aTree = arbitrary :: Gen (Tree Int String)


--- After insertion, a lookup with the same key yields the inserted value        
p_insert = forAll aTree (\t -> 
             forAll arbitrary (\k ->
               forAll arbitrary (\v ->
                lookup (insert t k v) k == Just v)))

--- After deletion of a key, lookup results in Nothing
p_delete = forAll aTree (\t ->
            not (null t) ==> forAll (elements (keys t)) (\k ->
                lookup (delete t k) k == Nothing))

Drugie prawo (lub właściwość) możemy odczytać w następujący sposób: W przypadku wszystkich dowolnych drzew tnastępujące są następujące: jeśli tnie jest puste, to dla wszystkich kluczy ktego drzewa będzie trzymać to spojrzenie kw drzewie, które jest wynikiem usunięcia kz t, wynikiem będzie Nothing(co oznacza: nie znaleziono).

Sprawdza to poprawność działania w celu usunięcia istniejącego klucza. Jakie przepisy powinny regulować usuwanie nieistniejącego klucza? Z pewnością chcemy, aby powstałe drzewo było takie samo jak drzewo, z którego usunęliśmy. Możemy to łatwo wyrazić:

p_delete_nonexistant = forAll aTree (\t ->
                          forAll arbitrary (\k -> 
                              k `notElem` keys t ==> delete t k == t))

W ten sposób testowanie jest naprawdę zabawne. Poza tym, gdy nauczysz się czytać właściwości szybkiego sprawdzania, służą one jako specyfikacja do przetestowania na maszynie .

Nie do końca rozumiem, co oznacza połączona odpowiedź poprzez „osiągnięcie modułowości poprzez prawa matematyczne”, ale myślę, że mam pojęcie o tym, co to znaczy.

Sprawdź Functor :

Klasa Functor jest zdefiniowana w następujący sposób:

 class Functor f where
   fmap :: (a -> b) -> f a -> f b

Nie zawiera przypadków testowych, a raczej kilka przepisów, które należy spełnić.

Wszystkie instancje Functora powinny być zgodne:

 fmap id = id
 fmap (p . q) = (fmap p) . (fmap q)

Powiedzmy teraz, że implementujesz Functor( źródło ):

instance  Functor Maybe  where
    fmap _ Nothing       = Nothing
    fmap f (Just a)      = Just (f a)

Problem polega na sprawdzeniu, czy Twoje wdrożenie jest zgodne z prawem. Jak ty to robisz?

Jednym z podejść jest pisanie przypadków testowych. Podstawowym ograniczeniem tego podejścia jest to, że weryfikujesz zachowanie w skończonej liczbie przypadków (powodzenia, wyczerpujące testowanie funkcji z 8 parametrami!), A zatem zaliczenie testów nie może zagwarantować niczego poza pozytywnym wynikiem testów.

Innym podejściem jest zastosowanie rozumowania matematycznego, tj. Dowodu, opartego na faktycznej definicji (zamiast na zachowaniu w ograniczonej liczbie przypadków). Chodzi o to, że dowód matematyczny może być bardziej skuteczny; zależy to jednak od tego, jak podatny jest twój program na dowód matematyczny.

Nie mogę przeprowadzić cię przez faktyczny dowód formalny, że powyższa Functorinstancja jest zgodna z prawem, ale postaram się przedstawić zarys tego, jak mógłby wyglądać ten dowód:

1. fmap id = id
   • Jeśli mamy Nothing
     • fmap id Nothing= Nothingw części 1 wdrożenia
     • id Nothing= Nothingz definicjiid
   • Jeśli mamy Just x
     • fmap id (Just x)= Just (id x)= Just xw części 2 wdrożenia, a następnie według definicjiid
2. fmap (p . q) = (fmap p) . (fmap q)
   • Jeśli mamy Nothing
     • fmap (p . q) Nothing= Nothingprzez część 1
     • (fmap p) . (fmap q) $ Nothing= (fmap p) $ Nothing= Nothingprzez dwa zastosowania części 1
   • Jeśli mamy Just x
     • fmap (p . q) (Just x)= Just ((p . q) x)= Just (p (q x))według części 2, a następnie według definicji.
     • (fmap p) . (fmap q) $ (Just x)= (fmap p) $ (Just (q x))= Just (p (q x))przez dwa zastosowania części drugiej

„Strzeż się błędów w powyższym kodzie; udowodniłem tylko, że jest poprawny, a nie wypróbowałem”. - Donald Knuth

W idealnym świecie programiści są doskonali i nie popełniają błędów, więc nie ma błędów.

W idealnym świecie informatycy i matematycy są również doskonali i nie popełniają błędów.

Ale nie żyjemy w idealnym świecie. Dlatego nie możemy polegać na programistach, którzy nie popełniają błędów. Ale nie możemy zakładać, że żaden informatyk, który dostarczy matematyczny dowód, że program jest poprawny, nie popełnił żadnych błędów w tym dowodzie. Dlatego nie zwracałbym uwagi na nikogo, kto próbowałby udowodnić, że jego kod działa. Napisz testy jednostkowe i pokaż mi, że kod zachowuje się zgodnie ze specyfikacjami. Nic innego mnie nie przekona.