Są języki dynamicznie typowane i są języki statycznie typowane. Ja wyznaję wyższość języków ze statycznym typowaniem, ale są różne opinie. Dzisiaj spojrzymy na to jak wygląda sprawdzanie typów podczas kompilacji.

Weryfikacja

W standardowym języku programowania, wywodzącym się z rodziny C, każda deklaracja zmiennej, argumentu, funkcji, jest opatrzona w informację o typie. Pozwala to na weryfikację typów.

Zaopatrzymy się więc w jakąś mapę <Identyfikator, Typ> i zaczniemy przechodzić przez nasze drzewo AST. Kluczem będzie posiadanie takiej struktury danych, która pozwoli na cofanie zmian przy wyjściu poza zasięg deklaracji.

Najpierw trzeba jeszcze się przejść po wszystkich funkcjach, klasach, metodach i zebrać informacje o ich typach.

W moim przypadku wygląda to jakoś tak:

1. Dla każdej funkcji zapisz metadane tej funkcji
2. Dla każdej klasy zapisz metadane tej klasy (w tym sygnatury metod i typy pól)
3. Dla każdej funkcji/metody sprawdź typy jej wnętrza
   • Dla każdego polecenia sprawdź typy podwyrażeń

Czyli jeśli mam deklarację

int x = y.f();

to muszę zrobić

• Sprawdź czy x nie było zadeklarowane wcześniej w tym bloku
• Sprawdź typ wyrażenia y.f() (wywołanie funkcji)
  • Sprawdź typ wyrażenia y.f (odwołanie do klasy)
    • Sprawdź typ wyrażenia y (zmienna)
      • Zajrzyj do mapy… Ok y ma typ T
    • Czy typ T ma członka f? Tak, typu int()
  • Sprawdź czy typy argumentów się zgadzają () vs ()
  • Ok, zwróć typ zwracany int
• Czy typ wyrażenia można przypisać na typ deklaracji int na int? Tak.

I tak robię dla wszystkich deklaracji, przypisań, returnów, itd.

W momencie kiedy sprawdzam metodę w klasie, to muszę dla identyfikatorów, których nie ma w mapie, sprawdzać czy są poprawnymi polami tej klasy i jeśli tak, to dopisuję do nich odwołanie do this.

Inferencja

Inferencja to proces, w którym to kompilator domyśla się jaki typ powinniśmy wstawić w dane miejsce. W przypadku języków takich jak Java, C#, czy w moim przypadku Latte, najprostszy system inferencji to inferencja lokalna. Pozwala ona nie pisać typów w deklaracjach.

var x = 10;
var y = "abc";

Na podstawie wyrażenia po prawej stronie przypisania, kompilator może domyślić się jakim typem zastąpić słowo var.

W językach programowania w paradygmacie funkcyjnym znacznie częściej mamy do czynienia z inferencją o znacznie szerszym zasięgu. W wielu przypadkach pozwala to na pisanie programu bez deklaracji typów, które są inferowane w całości przez kompilator.

f x y = x + y
> f :: Num a -> a -> a -> a

Aby to było możliwe to stosowane są różne systemy typów i algorytmy pozwalające na ich inferencję. Najpopularniejszym jest system Hindley–Milner (HM), który jest obecny w takich językach jak OCaml, F# i służy jako baza dla systemu typów w Haskellu.

Kod

Możesz zobaczyć jak w moim kompilatorze wygląda moduł weryfikacji typów. Nie powiem żeby to było wzorcowe rozwiązanie, i może być nieco nieczytelne na pierwszy rzut oka, ale działa.

W moim interpreterze, który robiłem w poprzednim semestrze, zaimplementowałem algorytm unifikacji typów HM, który możesz zobaczyć o tutaj. Aczkolwiek, ten kod jest jeszcze bardziej zawikłany.

Jeśli chcesz poczytać więcej o algorytmie unifikacji dla Haskella, to jest spoko artykuł o jego implementacji.