Wnioskowanie o typie — Type inference

Wnioskowanie o typie odnosi się do automatycznego wykrywania typu wyrażenia w języku formalnym . Należą do nich języki programowania i systemy typów matematycznych , ale także języki naturalne w niektórych gałęziach informatyki i językoznawstwa .

Wyjaśnienie nietechniczne

Typy w najbardziej ogólnym widoku mogą być powiązane z przeznaczeniem, sugerując i ograniczając czynności możliwe dla obiektu tego typu. Wiele rzeczowników w języku określa takie zastosowania. Na przykład słowo smycz wskazuje na inne zastosowanie niż słowo linia . Nazywanie czegoś stołem wskazuje na inne oznaczenie niż nazywanie tego drewnem opałowym , chociaż może to być zasadniczo to samo. Choć ich właściwości materiałowe sprawiają, że rzeczy nadają się do pewnych celów, podlegają one również szczególnym oznaczeniom. Dotyczy to zwłaszcza dziedzin abstrakcyjnych, czyli matematyki i informatyki, gdzie ostatecznie materiałem są tylko bity lub formuły.

Aby wykluczyć niepożądane, ale materialnie możliwe zastosowania, pojęcie typów jest definiowane i stosowane w wielu odmianach. W matematyce paradoks Russella zapoczątkował wczesne wersje teorii typów. W językach programowania typowymi przykładami są „błędy typu”, np. nakazanie komputerowi zsumowania wartości, które nie są liczbami. Chociaż jest to materialnie możliwe, wynik nie byłby już znaczący i być może katastrofalny dla całego procesu.

W typing wyrażenie jest przeciwieństwem typu. Na przykład , , i to oddzielne terminy z typem liczb naturalnych. Tradycyjnie po wyrażeniu następuje dwukropek i jego typ, np . . Oznacza to, że wartość jest typu . Ta forma jest również używana do deklarowania nowych imion, np. podobnie jak wprowadzenie nowej postaci do sceny słowami „detektyw Decker”. ${\ Displaystyle 4}$ $2+2$ $2\cdot 2$ $\mathrm {nat}$ $2:\mathrm {nat}$ $2$ $\mathrm {nat}$ $n:\mathrm {nat}$

W przeciwieństwie do opowieści, w której desygnacje rozwijają się powoli, przedmioty w językach formalnych często muszą być definiowane ich typem od samego początku. Ponadto, jeśli wyrażenia są niejednoznaczne, typy mogą być potrzebne, aby wyraźnie określić zamierzone użycie. Na przykład wyrażenie może mieć typ, ale może być również odczytywane jako liczba wymierna lub rzeczywista, a nawet jako zwykły tekst. $2$ $\mathrm {nat}$

W konsekwencji programy lub dowody mogą być tak obciążone typami, że pożądane jest wydedukowanie ich z kontekstu. Może to być możliwe dzięki zebraniu użycia wyrażeń niewpisanych (w tym niezdefiniowanych nazw). Jeśli na przykład w wyrażeniu użyto jeszcze niezdefiniowanej nazwy n , można by wywnioskować, że n jest co najmniej liczbą. Proces dedukowania typu z wyrażenia i jego kontekstu to wnioskowanie o typie . $n+2$

Generalnie nie tylko przedmioty, ale także czynności mają typy i mogą być wprowadzone po prostu przez ich użycie. W przypadku opowieści o Star Trek taką nieznaną aktywnością może być „przenoszenie”, które ze względu na przebieg opowieści jest właśnie wykonywane i nigdy formalnie nie wprowadzane. Niemniej jednak można wydedukować jego rodzaj (transport) po tym, co się dzieje. Dodatkowo zarówno obiekty, jak i czynności mogą być konstruowane z ich części. W takim otoczeniu wnioskowanie o typie staje się nie tylko bardziej złożone, ale także bardziej pomocne, ponieważ pozwala zebrać pełny opis wszystkiego w skomponowanej scenie, a jednocześnie jest w stanie wykryć sprzeczne lub niezamierzone zastosowania.

Sprawdzanie typu a wnioskowanie o typie

W typowaniu wyrażenie E jest przeciwieństwem typu T, formalnie zapisanego jako E : T. Zwykle typowanie ma sens tylko w pewnym kontekście, co jest tutaj pominięte.

W tym kontekście szczególnie interesujące są następujące pytania:

E: T? W tym przypadku podane jest zarówno wyrażenie E, jak i typ T. Czy E naprawdę jest T? Ten scenariusz jest znany jako sprawdzanie typu .
E: _? Tutaj znane jest tylko wyrażenie. Jeśli istnieje sposób na wyprowadzenie typu dla E, to dokonaliśmy wnioskowania o typie .
_ : T? Odwrotnie. Biorąc pod uwagę tylko typ, czy istnieje dla niego jakieś wyrażenie, czy typ nie ma wartości? Czy jest jakiś przykład T?

W przypadku prostego typu rachunku lambda wszystkie trzy pytania są rozstrzygalne . Sytuacja nie jest tak komfortowa, gdy dozwolone są bardziej wyraziste typy.

Rodzaje w językach programowania

Typy są cechą występującą w niektórych silnie statycznie typowanych językach. Jest to często charakterystyczne dla funkcjonalnych języków programowania w ogóle. Niektóre języki, które zawierają wnioskowanie o typie to C++11 , C# (od wersji 3.0), Chapel , Clean , Crystal , D , F# , FreeBASIC , Go , Haskell , Java (od wersji 10), Julia , Kotlin , ML , Nim , OCaml , Opa , Rpython , Rust , Scala , Swift , TypeScript , Vala , Dart i Visual Basic (od wersji 9.0). Większość z nich używa prostej formy wnioskowania o typie; układ typu Hindley-Milner może zapewnić pełniejszy typu wnioskowanie. Możliwość automatycznego wywnioskowania typów ułatwia wiele zadań programistycznych, pozostawiając programiście swobodę pominięcia adnotacji typu, jednocześnie umożliwiając sprawdzanie typu.

W niektórych językach programowania wszystkie wartości mają typ danych jawnie zadeklarowany w czasie kompilacji , co ogranicza wartości, które określone wyrażenie może przyjąć w czasie wykonywania . Coraz częściej kompilacja just-in-time sprawia, że rozróżnienie między czasem wykonywania a czasem kompilacji jest kwestią sporną. Jednak historycznie, jeśli typ wartości jest znany tylko w czasie wykonywania, języki te są wpisywane dynamicznie . W innych językach typ wyrażenia jest znany tylko w czasie kompilacji ; te języki są wpisywane statycznie . W większości języków z typami statycznymi typy funkcji wejściowych i wyjściowych oraz zmienne lokalne zwykle muszą być jawnie dostarczane przez adnotacje typu. Na przykład w C :

int add_one(int x) {
    int result; /* declare integer result */

    result = x + 1;
    return result;
}

Podpis tej definicji funkcji, int add_one(int x)deklaruje, że add_onejest to funkcja, która przyjmuje jeden argument jest liczbą całkowitą i zwraca liczbę całkowitą. int result;deklaruje, że zmienna lokalna resultjest liczbą całkowitą. W hipotetycznym języku obsługującym wnioskowanie o typie kod może być napisany w ten sposób:

add_one(x) {
    var result;  /* inferred-type variable result */
    var result2; /* inferred-type variable result #2 */

    result = x + 1;
    result2 = x + 1.0;  /* this line won't work (in the proposed language) */
    return result;
}

Jest to identyczne ze sposobem pisania kodu w języku Dart , z wyjątkiem tego, że podlega pewnym dodatkowym ograniczeniom opisanym poniżej. Możliwe byłoby wywnioskowanie typów wszystkich zmiennych w czasie kompilacji. W powyższym przykładzie kompilator wywnioskuje to resulti będzie xmiał typ integer, ponieważ stała 1jest typem integer, a zatem add_onejest to function int -> int. Zmienna result2nie jest używana w sposób legalny, więc nie miałaby typu.

W wyimaginowanym języku, w którym napisano ostatni przykład, kompilator zakładałby, że w przypadku braku informacji przeciwnych, +pobiera dwie liczby całkowite i zwraca jedną liczbę całkowitą. (Tak to działa na przykład w OCaml .) Z tego wnioskowania o typie może wywnioskować, że typ x + 1jest liczbą całkowitą, co oznacza, że resultjest liczbą całkowitą, a zatem zwracana wartość add_onejest liczbą całkowitą. Podobnie, ponieważ +wymaga , aby oba jego argumenty były tego samego typu, xmusi być liczbą całkowitą, a zatem add_oneprzyjmuje jedną liczbę całkowitą jako argument.

Jednak w kolejnym wierszu wynik2 jest obliczany przez dodanie 1.0liczby dziesiętnej za pomocą arytmetyki zmiennoprzecinkowej, co powoduje konflikt w użyciu xzarówno wyrażeń całkowitych, jak i zmiennoprzecinkowych. Prawidłowy algorytm wnioskowania o typie dla takiej sytuacji jest znany od 1958 r. i wiadomo, że jest poprawny od 1982 r. Powraca on do wcześniejszych wnioskowań i od samego początku używa najbardziej ogólnego typu: w tym przypadku zmiennoprzecinkowego. Może to jednak mieć szkodliwe implikacje, na przykład użycie liczby zmiennoprzecinkowej od samego początku może spowodować problemy z precyzją, których nie byłoby w przypadku typu całkowitego.

Często jednak używane są zdegenerowane algorytmy wnioskowania o typie, które nie mogą się cofnąć i zamiast tego generują komunikat o błędzie w takiej sytuacji. To zachowanie może być preferowane, ponieważ wnioskowanie o typie może nie zawsze być neutralne algorytmicznie, co ilustruje poprzedni problem z precyzją zmiennoprzecinkową.

Algorytm pośredniej ogólności niejawnie deklaruje wynik2 jako zmienną zmiennoprzecinkową, a dodawanie niejawnie konwertuje xna zmienną zmiennoprzecinkową. Może to być poprawne, jeśli konteksty wywołujące nigdy nie dostarczają argumentu zmiennoprzecinkowego. Taka sytuacja pokazuje różnicę między wnioskowaniem o typie , które nie obejmuje konwersji typu , a niejawną konwersją typu , która wymusza dane do innego typu danych, często bez ograniczeń.

Wreszcie istotną wadą złożonego algorytmu wnioskowania o typie jest to, że wynikowe rozwiązanie wnioskowania o typie nie będzie oczywiste dla ludzi (zwłaszcza z powodu nawrotów), co może być szkodliwe, ponieważ kod ma być przede wszystkim zrozumiały dla ludzi.

Niedawne pojawienie się kompilacji just-in-time pozwala na podejścia hybrydowe, w których typ argumentów dostarczanych przez różne konteksty wywołania jest znany w czasie kompilacji i może generować dużą liczbę skompilowanych wersji tej samej funkcji. Każdą skompilowaną wersję można następnie zoptymalizować pod kątem innego zestawu typów. Na przykład kompilacja JIT pozwala na istnienie co najmniej dwóch skompilowanych wersji add_one :

Wersja, która akceptuje dane wejściowe liczb całkowitych i używa niejawnej konwersji typu.

Wersja, która akceptuje liczbę zmiennoprzecinkową jako dane wejściowe i używa w całym tekście instrukcji zmiennoprzecinkowych.

Opis techniczny

Wnioskowanie o typie to możliwość automatycznego wywnioskowania, częściowo lub w całości, typu wyrażenia w czasie kompilacji. Kompilator często jest w stanie wywnioskować typ zmiennej lub sygnaturę typu funkcji, bez podania wyraźnych adnotacji typu. W wielu przypadkach możliwe jest całkowite pominięcie adnotacji typu z programu, jeśli system wnioskowania o typie jest wystarczająco niezawodny lub program lub język są wystarczająco proste.

Aby uzyskać informacje wymagane do wywnioskowania typu wyrażenia, kompilator albo zbiera te informacje jako agregację, a następnie redukcję adnotacji typu podanych dla jego podwyrażeń, albo poprzez niejawne zrozumienie typu różnych wartości atomowych (np. true : Bool; 42 : liczba całkowita; 3,14159 : liczba rzeczywista; itd.). Dzięki rozpoznaniu ewentualnej redukcji wyrażeń do niejawnie wpisanych wartości atomowych kompilator języka wnioskowania o typie jest w stanie skompilować program całkowicie bez adnotacji typu.

W złożonych formach programowania wyższego rzędu i polimorfizmu kompilator nie zawsze może wywnioskować tyle, a adnotacje typu są czasami konieczne do ujednoznacznienia. Na przykład wiadomo , że wnioskowanie o typie z rekurencją polimorficzną jest nierozstrzygalne. Ponadto adnotacje typu jawnego mogą służyć do optymalizacji kodu, zmuszając kompilator do użycia bardziej szczegółowego (szybszego/mniejszego) typu niż wywnioskował.

Niektóre metody wnioskowania o typie są oparte na teoriach spełniania ograniczeń lub spełnialności modulo .

Przykład

Na przykład funkcja Haskellamap stosuje funkcję do każdego elementu listy i może być zdefiniowana jako:

map f [] = []
map f (first:rest) = f first : map f rest

Wnioskowanie o typie mapfunkcji przebiega w następujący sposób. mapjest funkcją dwóch argumentów, więc jej typ jest ograniczony do postaci a → b → c. W Haskell wzorce []i (first:rest)zawsze pasują do list, więc drugi argument musi być typem listy: b = [d]dla jakiegoś typu d. Jego pierwszy argument fjest stosowany do argumentu first, który musi mieć typ d, odpowiadający typowi w argumencie listy, więc f :: d → e( ::oznacza "jest typu") dla pewnego typu e. Wartość zwracana przez map f, w końcu, jest listą tego, co fprodukuje, więc [e].

Składanie części razem prowadzi do map :: (d → e) → [d] → [e]. Nie ma nic szczególnego w zmiennych typu, więc można je zmienić jako

map :: (a → b) → [a] → [b]

Okazuje się, że jest to również najbardziej ogólny typ, ponieważ nie obowiązują żadne dalsze ograniczenia. Ponieważ wywnioskowany typ mapjest parametrycznie polimorficzny , typ argumentów i wyników fnie jest wywnioskowany, ale pozostawiony jako zmienne typu, dzięki czemu mapmożna go zastosować do funkcji i list różnych typów, o ile rzeczywiste typy pasują do każdego wywołania .

Algorytm wnioskowania typu Hindley-Milner

Algorytm użyty po raz pierwszy do wnioskowania o typie jest obecnie nieformalnie nazywany algorytmem Hindleya-Milnera, chociaż algorytm powinien być właściwie przypisany Damasowi i Milnerowi.

Źródłem tego algorytmu jest algorytm wnioskowania o typie dla prostego typu rachunku lambda, który został opracowany przez Haskella Curry'ego i Roberta Feysa w 1958. W 1969 J. Roger Hindley rozszerzył tę pracę i udowodnił, że ich algorytm zawsze wnioskował najbardziej ogólny typ. W 1978 roku Robin Milner , niezależnie od prac Hindleya, dostarczył równoważny algorytm, Algorytm W . W 1982 roku Luis Damas w końcu udowodnił, że algorytm Milnera jest kompletny i rozszerzył go o obsługę systemów z odniesieniami polimorficznymi.

Skutki uboczne używania najbardziej ogólnego typu

Z założenia wnioskowanie o typie, zwłaszcza poprawne (z wstecznym śledzeniem) wnioskowania o typie, wprowadzi użycie najbardziej ogólnego odpowiedniego typu, jednak może to mieć konsekwencje, ponieważ bardziej ogólne typy nie zawsze mogą być neutralne algorytmicznie, typowe przypadki to:

liczba zmiennoprzecinkowa jest uważana za ogólny typ liczby całkowitej, podczas gdy zmiennoprzecinkowa wprowadzi problemy z precyzją
typy wariantowe/dynamiczne są uważane za ogólny typ innych typów, które wprowadzą reguły rzutowania i porównania, które mogą być różne, na przykład takie typy używają operatora „+” zarówno dla dodawania liczb, jak i łączenia ciągów, ale jaka operacja jest wykonywana jest wyznaczane dynamicznie, a nie statycznie

Wnioskowanie o typie dla języków naturalnych

Algorytmy wnioskowania o typie zostały wykorzystane do analizy języków naturalnych, a także języków programowania. Algorytmy wnioskowania o typie są również używane w niektórych systemach indukcji gramatycznej i systemach gramatycznych opartych na ograniczeniach dla języków naturalnych.

Bibliografia

Linki zewnętrzne

Zarchiwizowana wiadomość e-mail od Rogera Hindleya wyjaśnia historię wnioskowania o typie
Wnioskowanie o typie polimorficznym autorstwa Michaela Schwartzbacha zawiera przegląd wnioskowania o typie polimorficznym.
Basic Typechecking paper autorstwa Luca Cardelli, opisuje algorytm, zawiera implementację w Modula-2
Implementacja wnioskowania typu Hindley-Milner w Scali , Andrew Forrest (pobrano 30 lipca 2009)
Implementacja Hindley-Milner w Perl 5, Nikita Borisov w Wayback Machine (archiwum 18 lutego 2007)
Co to jest Hindley-Milner? (i dlaczego jest fajnie?) wyjaśnia Hindley-Milner, przykłady w Scala

Languages

In other projects