Algorytmy sprawdzania typu

Zaczynam osobiste badanie bibliograficzne algorytmów sprawdzania typu i chcę uzyskać wskazówki. Jakie są najczęściej stosowane algorytmy sprawdzania typu, strategie i techniki ogólne?

Szczególnie interesują mnie złożone algorytmy sprawdzania typu, które zostały zaimplementowane w powszechnie znanych, silnie statycznych językach, takich jak na przykład C ++, Java 5+, Scala lub inne. IE, algorytmy sprawdzania typów, które nie są bardzo proste ze względu na bardzo proste pisanie w języku bazowym (jak Java 1.4 i poniżej).

Sam nie jestem zainteresowany konkretnym językiem X, Y lub Z. Interesują mnie algorytmy sprawdzania typu, niezależnie od języka, na który są kierowane. Jeśli podasz odpowiedź typu „język L, o którym nigdy nie słyszałeś, który jest mocno wpisany, a pisanie jest złożone, masz algorytm sprawdzania typu, który wykonuje A, B i C, sprawdzając X i Y za pomocą algorytmu Z” lub „ strategia X i Y zastosowana w Scali oraz wariant Z A zastosowany w C # są fajne ze względu na funkcje R, S i T, które działają w ten sposób ", to odpowiedzi są dobre.

— Victor Stafusa
źródło

Może powinieneś edytować to pytanie, aby zapytać o sprawdzanie typu dla jednego określonego języka. Otwarte pytania w stylu listy są ogólnie odradzane w SE (chociaż ta konkretna strona nie ma jeszcze żadnych zasad w tym zakresie). Ponadto: <type-system-elitist> System typów Java nie jest złożony </type-system-elitist>.

— sepp2k

Być może pytanie można by sformułować bardziej szczegółowo, ale nie sądzę, że powinno zostać zamknięte.

— Dave Clarke

@ sepp2k: Wiem, że jest trochę szeroki, ale tak się skończyło, ponieważ nie chcę ograniczać użyteczności odpowiedzi. BTW, nie rozumiem, co chcesz powiedzieć z „<type-system-elitist> System typów Java nie jest skomplikowany </type-system-elitist>”. System Java w wersji 1.4 i niższej był w rzeczywistości prosty, ale odrobina ogólnych w Javie 5 stała się o wiele bardziej złożona.

— Victor Stafusa,

Pytanie o jeden konkretny język sprawiłoby, że pytanie byłoby bardziej nieodpowiednie dla tej witryny, imho. Pytanie może dotyczyć ogólnych technik.

— Raphael

@Victor Podstawowym narzędziem są gramatyki atrybutów . Być może nie będziesz w stanie zrobić z nimi wszystkich niegodziwych rzeczy, jakie możesz sobie wyobrazić, ale są one dobrym punktem wyjścia.

— Raphael

Odpowiedzi:

Większość badań w rzeczywistości nie publikuje algorytmów sprawdzania typu dla pełnych języków programowania. Znajdziesz niektóre formalizacje dużej części systemów typów dla pełnych języków programowania, takie jak prace wykonane przez Drossopoulou i Eisenbacha dla Javy lub prace Nipkova i in. Nad C ++ . Częściej jednak można znaleźć systemy typów tylko dla niektórych podstawowych części języka (przykładem jest Featherweight Java) lub dla podstawowych koncepcji języka, takich jak lokalne podejście do scala .

Na konferencjach takich jak POPL i ICFP można znaleźć wiele algorytmów sprawdzania typów dla określonych rodzajów systemów typów oraz nowatorskie podejścia, takie jak dwukierunkowe i trójkierunkowe sprawdzanie typów.

Mówiąc bardziej ogólnie, prawdopodobnie musisz wiedzieć o algorytmie Damas-Milner , wnioskowaniu o typach lokalnych, dwukierunkowym i tridirectional sprawdzaniu typów, a następnie rozwinąć, podążając za odnośnikami w artykułach i korzystając z wyszukiwarki Google, aby znaleźć cytowane artykuły i bazować na nich opisane podejścia. Ponadto, jak zasugerowano powyżej, konferencje takie jak POPL, ICPF, ESOP, a nawet ECOOP i OOPSLA będą miały dokumenty związane z twoją misją.

— Dave Clarke
źródło

Afaik, system typów Scali został opracowany w projektach badawczych i dlatego został opublikowany. Kompilator jest również typu open source. Jednak nie zajrzałem do żadnego z nich.

— Raphael

Nie muszę wnioskować; Ja wiem , że istnieją opublikowane prace na systemie typu Scala. Roszczenie to można łatwo sprawdzić poprzez wyszukiwanie . Ponadto liczę kod źródłowy kompilatora jako wystarczającą publikację na temat algorytmu (pod warunkiem, że jest on zawarty w źródłach; zakładam, że tak, ale nie sprawdziłem). Moje wstępne stwierdzenie było dwuznaczne, prawdziwe, ale twoja reakcja wydaje się nieuzasadniona.

— Raphael

Podstawowym narzędziem są gramatyki atrybutów . Być może nie będziesz w stanie zrobić z nimi wszystkich niegodziwych rzeczy, jakie możesz sobie wyobrazić, ale są one dobrym punktem wyjścia.

Zasadniczo można przejść od góry do dołu i / lub od dołu po abstrakcyjnym drzewie składni programu i przekazywać informacje. Na przykład można przekazać informacje o typie zasięgu globalnego (np. Klasy i ich elementy) w dół i określić typ wyrażeń rekurencyjnie, tj. Od dołu do góry, przekazując typy wynikowe w górę.

Znajdź wyjaśnienia i przykłady na slajdach tutaj (rozdział 5).

— Raphael
źródło

Czy ktoś ma lepsze referencje? Chyba muszę kupić Dragonbooka lub Wilhelma / Maurera jednego z tych dni ...

— Raphael

Narzędzie JastAdd to doskonały, nowoczesny system kompilatora kompilatorów oparty na gramatyce atrybutów referencyjnych. Wykorzystaliśmy go w wielu projektach.

— Dave Clarke