Tam gdzie statyczne typowanie nie wystarcza...

tam pojawia się... No właśnie, co? Zanim o tym, najpierw napiszę trochę o problemach z typowaniem. Statyczne typowanie daje nam pewność, że nigdy nie przekażemy innego typu do funkcji niż tego oczekuje. W językach dynamicznych często musimy pisać dodatkowe testy jednostkowe aby mieć jakąś dozę pewności, że dana funkcja zachowa się poprawnie dla niepoprawnego typu. Dla przykładu co ma zrobić funkcja zliczająca elementy w tablicy jeśli zamiast tablicy przekażemy jej liczbę? Mamy kilka możliwości:

• zwracamy 0 - zazwyczaj nie wywoła to od razu większych problemów, gdyż kod wykorzystujący taką funkcję jest raczej przygotowany na obsługę pustej tablicy. Niestety w ten sposób ukrywamy błąd, którym jest oczywiście przekazanie liczby zamiast tablicy. Znalezienie go przy takim rozwiązaniu może być kłopotliwe.
• zwracamy ujemną wartość - ujemna liczba elementów tablicy nie ma sensu więc może to sygnalizować jakiś błąd. Problem w tym, że wszędzie, gdzie używamy takiej funkcji musielibyśmy się ubezpieczyć na taką ewentualność. Tutaj znów potrzebowalibyśmy sporej liczby testów jednostkowych by jakoś to wymusić. Jeżeli tego nie zrobimy to istnieje ryzyko, że ktoś np. będzie coś przemnażał przez ujemną liczbę co znów może być trudne do wykrycia (choć łatwiejsze niż w przypadku zwracania 0).
• rzucamy wyjątek - błąd ukaże się nam od razu więc będzie łatwiejszy w lokalizacji. Tyle, że znów musielibyśmy się przed tym zabezpieczyć w miejscach, gdzie wykorzystujemy taką funkcję. Jeżeli tego nie zrobimy to cała aplikacja się po prostu wywali. Zatem i w tym wypadku potrzebujemy sporej liczby testów.

Wszystkie te rozwiązania mają jedną zasadniczą wadę w stosunku do statycznego typowania. Musimy dopisać sporą liczbę testów by móc wykryć błędy przed uruchomieniem aplikacji. W językach ze statycznym typowaniem, błąd zostanie wychwycony już przez kompilator/interpreter więc testy dla takich problemów są zbędne. No ale czy zawsze?

Typ a wartość

Czasami mimo używania statycznych typów i tak będziemy mieli problem. Dla przykładu weźmy sobie funkcję liczącą średnią z listy liczb. Czyli przyjmujemy sobie taką listę liczb, sumujemy jej elementy i dzielimy przez ich liczbę. A co jeśli przekazana lista jest pusta? Mielibyśmy dzielenie przez 0. Statyczne typowanie nas przed tym nie ustrzeże bo pusta lista to też lista (jest tego samego typu, tak jak 0 i 1). Mamy więc dwa wyjścia. Albo korzystamy z tych samych rozwiązań, które opisałem wyżej albo tworzymy dwa typy danych: jeden to lista pusta, a drugi to lista niepusta. Problem z dwoma typami danych jest taki, że pisanie w ten sposób byłoby raczej karkołomne. W Haskellu wszędzie, gdzie zwracaliśmy np. [Int] teraz mielibyśmy coś w rodzaju Either EmptyList (NotEmptyList Int). Wychodzi więc na to, że nie pozostaje nam nic innego jak pisanie testów i modlenie się przed wrzuceniem tego na produkcję, że wszystko zadziała. Na szczęście mamy jeszcze jedno wyjście (przynajmniej w Haskellu).

LiquidHaskell

LiquidHaskell to w skrócie dodatkowy walidator kodu Haskella, który umożliwia nam pisanie w komentarzach pewnych dodatkowych logicznych warunków co do wartości danego typu. Np. w powyższym przykładzie moglibyśmy dla funkcji liczącej średnią zapisać warunek, że nie przyjmuje ona listy pustej. Warunek ten będzie sprawdzony przed uruchomieniem aplikacji, a oto właśnie nam chodzi. Tylko, że jak to działa?

Najlepiej będzie pokazać to na przykładzie. Weźmy sobie przykładową implementację gry FizzBuzz. Gra polega na wymawianiu kolejnych liczb ale jeśli są one podzielne przez 3 to mówimy "Fizz", jeśli przez 5 to "Buzz", a jeśli przez 3 i 5 to "FizzBuzz". Oto przykładowa implementacja w Haskellu:

Przykładowy wynik działania programu:

Implementacja jest bardzo prosta. Jest też bardzo podatna na błędy. Np. weźmy sobie funkcję numberType i zamieńmy Fizz, Buzz, FizzBuzz na Normal i. Program skompiluje się bez problemu, a aplikacja będzie działać błędnie.

Teraz przyjrzyjmy się implementacji z wykorzystaniem LiquidHaskell:

Różni się ona tylko komentarzami, które są interpretowane przez program o nazwie liquid, który jest dostępny po zainstalowaniu LiquidHaskell. Co możemy z nich wyczytać? Dla przykładu weźmy tę linijkę: Normal (i :: {v:Int | v mod 3 /= 0 && v mod 5 /= 0}). Mówi ona o tym, że konstruktor Normal może przyjąć liczbę i, która jest typu Int ale tylko taką, która nie jest podzielna przez 3 i przez 5. No to wypróbujmy to. Spróbujmy zrobić tak jak poprzednio czyli w funkcji numberType we wszystkich warunkach wpisać Normal i. Po tej zmianie uruchamiamy liquid fizzbuzz.hs i otrzymujemy:

liquid pokazuje nam, że w liniach 31, 32, 33 (czyli tam gdzie zmienialiśmy) nie zgadzają się typy. Dla przykładu w linii 31 oczekiwano typu Int, który nie jest podzielny przez 3 ani przez 5 ale nic na to nie wskazuje. Zauważmy, że wszystkie dane do programu są wczytywane w trakcie jego działania. Zatem liquid musi interpretować wszystkie ify w naszym kodzie by móc czegokolwiek dowodzić. Nie wymaga on więc od nas innego pisania kodu niż zwykle.

Podsumowanie

Jak widać LiquidHaskell to potężne narzędzie. Oczywiście wydłuża to sprawdzanie (i pisanie) kodu ale jak się okazuje w praktyce nie potrzeba wcale dokładać wielu dodatkowych warunków by pozbyć się sporej liczby testów jednostkowych. Taka koncepcja jest szerzej znana jako dependent types i istnieje nawet kilka języków, które takie typy posiadają. Problemem jest oczywiście czas kompilacji takich programów i jak się wydaje LiquidHaskell stara się ten problem rozwiązać. Więcej można poczytać w samouczku.