Kategoryzacja systemów typów (mocna / słaba, dynamiczna / statyczna)

W skrócie: w jaki sposób kategoryzowane są systemy typów w kontekście akademickim; w szczególności, gdzie mogę znaleźć renomowane źródła, które wyraźnie rozróżniają różne systemy typów?

W pewnym sensie trudność związana z tym pytaniem nie polega na tym, że nie mogę znaleźć odpowiedzi, ale raczej na tym, że mogę znaleźć zbyt wiele i żadne z nich nie wyróżnia się jako poprawne. Tło stanowi próbę ulepszenia artykułu na wiki Haskell o pisaniu na maszynie , który obecnie ma następujące różnice:

• Bez pisania: w języku nie ma pojęcia typów ani z perspektywy typowania: w języku jest dokładnie jeden typ. Język asemblera ma tylko „wzorzec bitowy”, Rexx i Tk mają tylko „tekst”, rdzeń MatLab ma tylko typ „macierz o złożonej wartości”.
• Słabe pisanie: Istnieje tylko kilka wyróżnionych typów i być może synonimy typów dla kilku typów. Np. C używa liczb całkowitych dla logicznych, liczb całkowitych, znaków, zestawów bitów i wyliczeń.
• Mocne pisanie: drobnoziarnisty zestaw typów, takich jak w Adzie, wirthian (Pascal, Modula-2), Eiffel

Jest to całkowicie sprzeczne z moją osobistą percepcją, która bardziej przypominała:

• Słabe pisanie: Obiekty mają typy, ale są domyślnie konwertowane na inne typy, gdy wymaga tego kontekst. Na przykład Perl, PHP i JavaScript to wszystkie języki, w których "1"można używać mniej więcej w dowolnym kontekście 1.
• Silne pisanie: Obiekty mają typy i nie ma niejawnych konwersji (chociaż można je symulować przy przeciążeniu), więc użycie obiektu w niewłaściwym kontekście jest błędem. W Pythonie indeksowanie tablicy ciągiem lub liczbą zmiennoprzecinkową powoduje wyjątek TypeError; w Haskell zakończy się niepowodzeniem w czasie kompilacji.

Poprosiłem o opinie na ten temat od innych osób bardziej doświadczonych w tej dziedzinie niż ja, a jedną z tych cech scharakteryzowałem:

• Słabe pisanie: Wykonywanie nieprawidłowych operacji na danych nie jest kontrolowane ani odrzucane, a jedynie powoduje nieprawidłowe / arbitralne wyniki.
• Silne pisanie: Operacje na danych są dozwolone tylko wtedy, gdy dane są zgodne z operacją.

Jak rozumiem, pierwsza i ostatnia charakterystyka nazwałaby C słabym typem, druga nazwałaby to silnym typem. Pierwszy i drugi wywoływałyby słaby typ Perla i PHP, a trzeci wywoływałby je silnie napisane. Wszyscy trzej opisaliby Python jako silnie wpisany.

Myślę, że większość ludzi powiedziałaby mi „no cóż, nie ma konsensusu, nie ma akceptowanego znaczenia terminów”. Jeśli osoby te są błędne, byłbym szczęśliwy, aby usłyszeć o tym, ale jeśli mają rację, to jak mają naukowcy CS opisać i porównać systemy typu? Jakiej terminologii mogę użyć, która jest mniej problematyczna?

Jako powiązane pytanie czuję, że dynamiczne / statyczne rozróżnienie jest często podawane w kategoriach „czasu kompilacji” i „czasu wykonywania”, co uważam za niezadowalające, biorąc pod uwagę, że to, czy język jest kompilowany, nie jest jego własnością jako jego implementacje. Uważam, że powinien istnieć czysto semantyczny opis pisania dynamicznego kontra statycznego; coś w stylu „języka statycznego to taki, w którym można wpisać każde podwyrażenie”. Byłbym wdzięczny za wszelkie przemyślenia, szczególnie odniesienia, które nadają temu pojęciu jasności.

Historycznie termin „silnie typowany język programowania” pojawił się w latach 70. w reakcji na istniejące powszechnie używane języki programowania, z których większość zawierała dziury. Kilka przykładów:

• W Fortranie istniały rzeczy zwane obszarami pamięci „WSPÓLNE”, które mogły być współużytkowane przez moduły, ale nie było sprawdzania, czy każdy moduł deklaruje zawartość pamięci WSPÓLNEJ tego samego typu. Tak więc jeden moduł może zadeklarować, że konkretny wspólny blok pamięci ma liczbę całkowitą, a inny liczbę zmiennoprzecinkową, w wyniku czego dane zostaną uszkodzone. Fortran miał także instrukcje „RÓWNOWAŻNOŚĆ”, w których to samym magazynie można było zadeklarować, że zawiera dwa różne obiekty różnych typów.

• W Algolu 60 typ parametrów procedury został zadeklarowany jako „procedura”, bez określania typów parametrów procedury. Można więc założyć, że parametr procedury był procedurą akceptującą liczby całkowite, ale przekazał jako argument procedurę akceptacji rzeczywistej. Spowodowałoby to ten sam rodzaj korupcji, co oświadczenia WSPÓLNE i RÓWNOWAŻNE. (Jednak Algol 60 wyeliminował starsze problemy).

• W Pascalu dodano „zapisy wariantów”, które były prawie dokładnie tak, jak stare oświadczenia EQUIVALENCE.

• W C dodano „rzutowania typu”, dzięki czemu każdy typ danych może być ponownie interpretowany jako dane innego typu. Była to raczej celowa luka przeznaczona dla programistów, którzy podobno wiedzą, co robią.

Silnie napisane języki zaprojektowane w latach 70. miały na celu wyeliminowanie wszystkich takich dziur. Jeśli zagłębisz się w to, co to oznacza, oznacza to zasadniczo, że reprezentacje danych są chronione. Nie można wyświetlić obiektu danych jednego typu jako obiektu innego typu, który ma taki sam wzór bitowy jak jego wewnętrzna reprezentacja. Teoretycy zaczęli używać terminu „niezależność reprezentacji”, aby scharakteryzować tę właściwość, zamiast niejasnego pojęcia „silnego pisania”.

Należy zauważyć, że języki dynamicznie wpisywane, takie jak Lisp, które wykonują pełne sprawdzanie typów w czasie wykonywania, są „mocno wpisywane” w sensie ochrony reprezentacji. Jednocześnie statycznie wpisane języki straciłyby niezależność reprezentacji, chyba że sprawdzą granice tablic. Nie są więc „mocno wpisane” w ścisłym tego słowa znaczeniu. Z powodu tych anomalnych konsekwencji termin „mocno wpisany na maszynie” przestał być używany po latach 70-tych. Kiedy Departament Obrony USA opracował rygorystyczne wymagania dotyczące projektowania Ady, obejmowały one wymóg, aby język był „silnie pisany”. (Wydaje się, że w tamtym czasie uważano, że idea „silnego pisania” była oczywista. Nie podano definicji. ) Wszystkie propozycje językowe przedstawione w odpowiedzi twierdziły, że są „silnie napisane”. Kiedy Dijkstra przeanalizował wszystkie propozycje językowe, stwierdził, że żadna z nich nie została napisana na maszynie i w rzeczywistości nie było nawet jasne, co oznacza ten termin. Zobacz raportEWD663 . Widzę jednak, że termin ten powraca teraz do użytku przez młodsze pokolenie badaczy, którzy nie znają burzliwej historii tego terminu.

Termin „typowanie statyczne” oznacza, że ​​wszystkie sprawdzanie typu odbywa się statycznie i nie wystąpią żadne błędy typu w czasie wykonywania. Jeśli język jest również mocno wpisany, oznacza to, że tak naprawdę nie ma błędów podczas wykonywania. Jeśli z drugiej strony są dziury w systemie typów, brak błędów typu w czasie wykonywania nic nie znaczy. Wyniki mogą być całkowicie zepsute.

Nowa debata na temat „silnego i słabego pisania” wydaje się dotyczyć tego, czy niektóre konwersje typów powinny być dozwolone. Zezwalanie na ciąg, w którym wymagana jest liczba całkowita, jest „słabym typowaniem” według tych ludzi. Ma to pewien sens, ponieważ próba konwersji łańcucha na liczbę całkowitą może się nie powieść, jeśli łańcuch nie reprezentuje liczby całkowitej. Jednak konwersja liczby całkowitej na ciąg nie ma tego problemu. Czy według tych ludzi byłby to przypadek „słabego pisania”? Nie mam pojęcia. Zauważam, że dyskusje Wikipedii na temat „słabego pisania” nie cytują żadnych recenzowanych publikacji. Nie wierzę, że jest to spójny pomysł.

Dodano uwagę : podstawową kwestią jest to, że termin „mocne pisanie na klawiaturze” nie wszedł w życie jako termin techniczny o ścisłej definicji. Było to bardziej jak niektórzy projektanci języków: „nasz system pisma jest silny; wyłapuje wszystkie błędy pisma; nie ma dziur”, a więc, kiedy opublikowali swój projekt języka, twierdzili, że był „mocno wpisany” . To było modne słowo, które brzmiało dobrze i ludzie zaczęli go używać. Artykuł Cardelli-Wegner był pierwszym, który widziałem, w którym przedstawiono analizę tego, co to znaczy. Mój post tutaj należy traktować jako rozwinięcie ich stanowiska.

Artykuł, który Uday Reddy znalazł w swojej odpowiedzi, On Understanding Types, Data Abstraction and Polymorphism (1985), daje następujące odpowiedzi:

Mówi się, że języki programowania, w których typ każdego wyrażenia można określić za pomocą statycznej analizy programu, są typowane statycznie. Wpisywanie statyczne jest użyteczną właściwością, ale wymóg, aby wszystkie zmienne i wyrażenia były powiązane z typem w czasie kompilacji, jest czasami zbyt restrykcyjny. Można go zastąpić słabszym wymogiem, że wszystkie wyrażenia mają być zgodne z typem, chociaż sam typ może być statystycznie nieznany; ogólnie można to zrobić, wprowadzając sprawdzanie typu w czasie wykonywania. Języki, w których wszystkie wyrażenia są zgodne z typem, nazywane są językami silnie typowanymi. Jeśli język jest silnie wpisany, jego kompilator może zagwarantować, że programy, które akceptuje, będą działać bez błędów typu. Ogólnie rzecz biorąc, powinniśmy dążyć do silnego pisania i, w miarę możliwości, stosować pisanie statyczne.

Autorytatywne odpowiedzi można znaleźć w artykule z ankiety Cardelli i Wegnera: O typach zrozumienia, abstrakcji danych i polimorfizmie .

Pamiętaj, że chociaż „mocne pisanie” ma przyjęte znaczenie, „słabe pisanie” nie. Każda awaria silnego pisania może być uważana za słabą, a ludzie mogą różnić się co do tego, jaki rodzaj awarii jest dopuszczalny, a co nie.