implementacja wnioskowania o typie

Widzę tutaj kilka interesujących dyskusji na temat pisania statycznego i dynamicznego. Generalnie wolę wpisywanie statyczne, ze względu na sprawdzanie typów kompilacji, lepiej udokumentowany kod itp. Zgadzam się jednak, że zaśmiecają one kod, jeśli są robione tak, jak robi to na przykład Java.

Więc zaraz zacznę budować własny funkcjonalny język stylów, a wnioskowanie o typie jest jedną z rzeczy, które chcę wdrożyć. Rozumiem, że to duży temat i nie próbuję tworzyć czegoś, czego wcześniej nie robiono, tylko podstawowe wnioskowanie ...

Jakieś wskazówki, co przeczytać, a które pomogą mi w tym? Najlepiej coś bardziej pragmatycznego / praktycznego w przeciwieństwie do bardziej teoretycznych tekstów teorii kategorii / teorii typów. Jeśli istnieje tekst do dyskusji na temat implementacji, zawierający struktury danych / algorytmy, byłoby to po prostu cudowne.

Znalazłem następujące zasoby pomocne w zrozumieniu wnioskowania o typie, w kolejności rosnącej trudności:

1. Rozdział 30 (Wnioskowanie o typach) ogólnodostępnej książki PLAI , Języki programowania: zastosowanie i interpretacja , szkicuje wnioskowanie o typie oparte na unifikacji.
2. Letni kurs Interpretowanie typów jako wartości abstrakcyjnych przedstawia eleganckich oceniających, sprawdzających typy, rekonstruktorów typów i wnioskujących używających Haskella jako metajęzyka.
3. Rozdział 7 (Typy) książki EOPL , Essentials of Programming Languages .
4. Rozdział 22 (Rekonstrukcja typów) książki TAPL , typy i języki programowania oraz odpowiadające im implementacje OCaml Recon and Fullrecon .
5. Rozdział 13 (Rekonstrukcja typu) nowej książki DCPL , Koncepcje projektowania w językach programowania .
6. Wybór prac naukowych .
7. Metoda TypeInference kompilatora Closure jest przykładem podejścia analizy przepływu danych do wnioskowania o typie, które jest lepiej dostosowane do języków dynamicznych niż podejście Hindlera Milnera.

Ponieważ jednak najlepszym sposobem uczenia się jest robienie tego, zdecydowanie sugeruję implementację wnioskowania o typie dla języka funkcjonalnego zabawki poprzez wykonanie zadania domowego z kursu języków programowania.

Polecam te dwie dostępne prace domowe w ML, które możesz wykonać w mniej niż jeden dzień:

1. PCF Interpreter ( rozwiązanie ) do rozgrzewki.
2. PCF Type Inference ( rozwiązanie ) do implementacji algorytmu W dla wnioskowania typu Hindley-Milner.

Te zadania pochodzą z bardziej zaawansowanego kursu:

1. Wdrażanie MiniML

2. Typy polimorficzne, egzystencjalne, rekurencyjne (PDF)

3. Dwukierunkowe sprawdzanie typów (PDF)

4. Podtytuł i obiekty (PDF)

Szkoda, że ​​duża część literatury na ten temat jest bardzo bogata. Ja też byłem na twoim miejscu. Pierwsze wprowadzenie do tematu dostałem z Języki programowania: aplikacje i interpretacja

http://www.plai.org/

Spróbuję podsumować abstrakcyjną ideę, a następnie szczegóły, które nie były dla mnie od razu oczywiste. Po pierwsze, można pomyśleć o wnioskowaniu o typie o generowaniu, a następnie rozwiązywaniu ograniczeń. Aby wygenerować ograniczenia, należy powtórzyć drzewo składni i wygenerować jedno lub więcej ograniczeń w każdym węźle. Na przykład, jeśli węzeł jest +operatorem, wszystkie operandy i wyniki muszą być liczbami. Węzeł, który stosuje funkcję, ma ten sam typ co wynik funkcji i tak dalej.

W przypadku języka bez let, możesz ślepo rozwiązać powyższe ograniczenia przez podstawianie. Na przykład:

(if (= 1 2) 
    1 
    2)

tutaj możemy powiedzieć, że warunek instrukcji if musi być logiczny, a typ instrukcji if jest taki sam, jak typ jej klauzul theni else. Ponieważ znamy liczby 1i 2jesteśmy liczbami, przez podstawienie wiemy, że ifstwierdzenie jest liczbą.

Tam, gdzie robi się nieprzyjemnie i czego przez chwilę nie mogłem zrozumieć, to niech:

(let ((id (lambda (x) x)))
    (id id))

Tutaj mamy powiązanie idz funkcją, która zwraca wszystko, co przekazałeś, inaczej znaną jako funkcja tożsamości. Problem polega na tym, że typ parametru funkcji xjest inny przy każdym użyciu id. Druga idto funkcja typua -> a , gdzie amoże być wszystko. Pierwsza jest typowa (a -> a) -> (a -> a). Jest to znane jako let-polimorfizm. Kluczem jest rozwiązanie więzów w określonej kolejności: najpierw rozwiąż ograniczenia dla definicji id. To będzie a -> a. Następnie świeże, oddzielne kopie typu idmożna podstawić do ograniczeń dla każdego miejsca id, na przykład a2 -> a2i a3 -> a3.

Nie było to łatwo wyjaśnione w zasobach internetowych. Wspomną o algorytmie W lub M, ale nie o tym, jak działają w zakresie rozwiązywania ograniczeń, ani dlaczego nie działa on na polimorfizm let: każdy z tych algorytmów wymusza uporządkowanie rozwiązywania ograniczeń.

Uważam, że ten zasób jest niezwykle pomocny w łączeniu algorytmów W, M i ogólnej koncepcji generowania i rozwiązywania ograniczeń razem. Jest trochę gęsty, ale lepszy niż wiele:

http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf

Wiele innych artykułów też jest fajnych:

http://people.cs.uu.nl/bastiaan/papers.html

Mam nadzieję, że pomoże to wyjaśnić nieco mroczny świat.

Oprócz Hindley Milner dla języków funkcjonalnych, innym popularnym podejściem do wnioskowania o typie dla języka dynamicznego jest abstract interpretation .

Idea abstrakcyjnej interpretacji polega na napisaniu specjalnego interpretera dla języka, zamiast utrzymywać środowisko konkretnych wartości (1, false, closure), działa na abstrakcyjnych wartościach, czyli typach (int, bool itp.). Ponieważ interpretuje program na wartościach abstrakcyjnych, dlatego nazywa się to interpretacją abstrakcyjną.

Pysonar2 to elegancka implementacja abstrakcyjnej interpretacji dla Pythona. Jest używany przez Google do analizy projektów w Pythonie. Zasadniczo służy visitor patterndo wysyłania wywołania oceny do odpowiedniego węzła AST. Funkcja gościa transform akceptuje wartość, contextw której zostanie oceniony bieżący węzeł, i zwraca typ bieżącego węzła.

Typy i języki programowania Benjamin C. Pierce

Lambda the Ultimate, zaczynając tutaj .