Badanie wnioskowania na podstawie typu strony wywołującej?

Próbuję dowiedzieć się więcej na temat sprawdzania typu całego programu i systemów wnioskowania o typie, które wykorzystują informacje z witryn wywołań funkcji do obliczania informacji o typie (oprócz standardowego podejścia do używania treści funkcji). Na przykład taki algorytm może użyć wywołania funkcji, na przykład, foo(1)aby wnioskować, że funkcja w foopobiera argumenty liczb całkowitych. Oczywiście skomplikowałoby to wnioskowanie i sprawiłoby, że czek nie był modułowy.

W każdym razie nie miałem szczęścia znaleźć badań dotyczących tego podejścia, prawdopodobnie dlatego, że nie znam właściwej terminologii opisującej to, o czym mówię. Jakieś wskazówki?

Prawie wszystkie systemy z wnioskowaniem typu wykorzystują do tego informacje z witryny wywołań. Przykłady obejmują Standard ML, OCaml, F # i Haskell. Wiele innych języków używa informacji o stronie wywoływania do wnioskowania o instancji parametru typu, takich jak Java, C #, Scala i Typed Racket. Często nazywa się to „Lokalne wnioskowanie typu”.

Po prostu opisałbym to, czego szukasz, jako „Wnioskowanie typu” i prawdopodobnie powinieneś zacząć od wyszukiwania tego, co jest powszechnie znane jako system „Hindley-Milner”. Strona Wikipedii zawiera rozsądne wprowadzenie i wskazówki do oryginalnych artykułów.

Miejscem do rozpoczęcia Lokalnego Wnioskowania jest oryginalny artykuł Pierce'a i Turnera, najlepiej przeczytać w wersji TOPLAS 2000 ( ACM , PDF ).

Możesz rzucić okiem na systemy typów dla typów skrzyżowań, które mogą dać ci coś takiego a :: Int -> Int | Bool -> Bool, dzięki czemu wiesz, że dwie specjalizacje są wystarczające Inti Boolmożesz użyć wnioskowania typowego dla wnioskowania o najbardziej ogólnych typach, a następnie analizy przepływu sterowania w celu zebrania rzeczywistych wpisz argumenty. W rzeczywistości istnieją podejścia hybrydowe (CFA wyrażone jako system typów i odwrotnie).

Mogą istnieć badania nad wnioskowaniem najmniej ogólnych typów zamiast większości ogólnych typów, ale nie jestem ich świadomy.

Jeśli chodzi o techniki implementacji polimorfizmu, istnieją dwa rozwiązania: 1) specjalizacja (pomyśl o szablonach C ++) 2) założenie jednolitej reprezentacji (pomyśl o kolekcjach w stylu C z void *).

W przypadku 2 nie jest potrzebny typ ze strony wywoływania podczas sprawdzania typu, a łatwiej jest obsługiwać oddzielną kompilację.

Zauważ, że mówimy tutaj o polimorfizmie parametrycznym, a wirtualne wywołania metod OO to zupełnie inna rzecz zwana polimorfizmem podtypu. Zauważ, że szablony C ++ obsługują zarówno coś w rodzaju polimorfizmu parametrycznego, jak i pisanie na klawiaturze, co jest kolejną formą polimorfizmu.