tło

Projektuję język jako projekt poboczny. Mam do tego działający asembler, analizator statyczny i maszynę wirtualną. Ponieważ mogę już skompilować i uruchomić nietrywialne programy z wykorzystaniem infrastruktury, którą zbudowałem, pomyślałem o wygłoszeniu prezentacji na moim uniwersytecie.

Podczas mojej rozmowy wspomniałem, że maszyna wirtualna zapewnia system typów, zapytano: „Do czego służy system typów? ”. Po odpowiedzi wyśmiewa mnie osoba zadająca pytanie.

Tak więc, chociaż prawie na pewno stracę reputację, zadając to pytanie, zwracam się do programistów.

Moje zrozumienie

Jak rozumiem, systemy typów są używane do zapewnienia dodatkowej warstwy informacji o bytach w programie, dzięki czemu środowisko wykonawcze, kompilator lub inna część maszyny wie, co zrobić z ciągami bitów, na których działa. Pomagają również w utrzymywaniu umów - kompilator (lub analizator kodu, środowisko wykonawcze lub dowolny inny program) może sprawdzić, czy w dowolnym momencie program działa na wartościach, na których programiści oczekują.

Typy mogą być również używane do dostarczania informacji tym ludzkim programistom. Na przykład znajduję tę deklarację:

function sqrt(double n) -> double;

bardziej przydatny niż ten

sqrt(n)

Ten pierwszy zawiera wiele informacji: że sqrtidentyfikator jest funkcją, przyjmuje jeden doublejako dane wejściowe, a drugi tworzy doublejako dane wyjściowe. Ten ostatni mówi, że jest to prawdopodobnie funkcja przyjmująca pojedynczy parametr.

Moja odpowiedź

Po zapytaniu „Do czego służy Twój system typów?” Odpowiedziałem w następujący sposób:

System typów jest dynamiczny (typy są przypisywane do wartości, a nie do zmiennych je przechowujących), ale silny bez zaskakujących reguł przymusu (nie można dodać ciągu do liczby całkowitej, ponieważ reprezentują one typy niezgodne, ale można dodać liczbę całkowitą do liczby zmiennoprzecinkowej) .

System typów jest używany przez maszynę wirtualną, aby upewnić się, że argumenty instrukcji są prawidłowe; i mogą być używane przez programistów, aby upewnić się, że parametry przekazane do ich funkcji są prawidłowe (tj. poprawnego typu).
System typów obsługuje podsieci i wielokrotne dziedziczenie (obie funkcje są dostępne dla programistów), a typy są uwzględniane, gdy używana jest dynamiczna wysyłka metod na obiektach - VM używa typów, aby sprawdzić, jaką funkcją jest dany komunikat zaimplementowany dla danego typu.

Kolejne pytanie brzmiało: „A w jaki sposób typ jest przypisywany do wartości?”. Wyjaśniłem więc, że wszystkie wartości są zapakowane w ramkę i mają wskaźnik wskazujący na strukturę definicji typu, która dostarcza informacji o nazwie typu, jakie komunikaty odpowiada i jakie typy dziedziczy.

Potem wyśmiewano mnie i moja odpowiedź została odrzucona z komentarzem „To nie jest prawdziwy system typów”.

Więc - jeśli to, co opisałem, nie kwalifikuje się jako „prawdziwy system typów”, co by to było? Czy ta osoba miała rację, że tego, co zapewniam, nie można uznać za system typów?

Wszystko to wydaje się dobrym opisem tego, co zapewniają systemy typu. A twoja implementacja wydaje się wystarczająco rozsądna do tego, co robi.

W przypadku niektórych języków nie potrzebujesz informacji o środowisku wykonawczym, ponieważ Twój język nie obsługuje wysyłania w czasie wykonywania (lub wykonujesz pojedyncze wysyłanie za pomocą vtables lub innego mechanizmu, więc nie potrzebujesz informacji o typie). W przypadku niektórych języków wystarczy mieć symbol / symbol zastępczy, ponieważ zależy Ci tylko na równości typów, a nie na nazwie i dziedziczeniu.

W zależności od środowiska osoba ta mogła chcieć większego formalizmu w systemie typów. Chcą wiedzieć, co możesz z tym udowodnić , a nie to, co programiści mogą z tym zrobić . Niestety jest to dość powszechne w środowisku akademickim. Chociaż akademicy robią takie rzeczy, ponieważ dość łatwo jest mieć wady w systemie typów, które pozwalają wymknąć się poprawności. Możliwe, że zauważyli jedną z nich.

Jeśli masz dodatkowe pytania, Typy i języki programowania są kanoniczną książką na ten temat i mogą pomóc ci nauczyć się rygorów potrzebnych naukowcom, a także terminologii, która pomoże opisać różne rzeczy.

Podoba mi się odpowiedź @ Telastyn, szczególnie ze względu na odniesienie do akademickiego zainteresowania formalizmem.

Pozwól mi dodać do dyskusji.

Co to jest system typów?

System typów to mechanizm definiowania, wykrywania i zapobiegania nielegalnym stanom programu. Działa poprzez definiowanie i stosowanie ograniczeń. Definicjami ograniczeń są typy , a aplikacjami ograniczeń są zastosowania typów , np. W deklaracji zmiennej.

Definicje typów zazwyczaj obsługują operatory kompozycji (np. Różne formy koniunkcji, jak w strukturach, podklasach i rozłączności, jak w wyliczeniach, związkach).

Ograniczenia, zastosowania typów, czasami pozwalają również operatorom kompozycji (np. Przynajmniej to, dokładnie to, to lub tamto, pod warunkiem, że coś innego się zachowuje).

Jeśli system typów jest dostępny w języku i stosowany w czasie kompilacji w celu umożliwienia wydawania błędów w czasie kompilacji, jest to system typu statycznego; zapobiegają one kompilacji wielu nielegalnych programów, nie mówiąc już o ich uruchomieniu, a tym samym zapobiegają stanom nielegalnych programów.

(System typu statycznego zatrzymuje działanie programu, niezależnie od tego, czy wiadomo (lub nierozstrzygalność), że program kiedykolwiek osiągnie ten niesłuszny kod, na który skarży się. System typu statycznego wykrywa pewne bzdury (naruszenia deklarowanych ograniczeń) i ocenia program błędnie, zanim się uruchomi).

Jeżeli system typów jest stosowany w czasie wykonywania, jest to system typu dynamicznego, który zapobiega niedozwolonym stanom programu: ale poprzez zatrzymanie programu w trakcie uruchamiania, a nie zapobieganie jego uruchomieniu.

Dość powszechną ofertą systemów typu jest zapewnienie zarówno statycznych, jak i dynamicznych funkcji.

O rany, cieszę się, że mogę odpowiedzieć na to pytanie najlepiej, jak potrafię. Mam nadzieję, że potrafię odpowiednio uporządkować myśli.

Jak wspomniano @Doval i pytający wskazał (choć niegrzecznie), tak naprawdę nie masz systemu typów. Masz system dynamicznych kontroli za pomocą znaczników, który jest ogólnie znacznie słabszy, a także znacznie mniej interesujący.

Pytanie „co to jest system typów” może być dość filozoficzne i moglibyśmy wypełnić książkę różnymi punktami widzenia na ten temat. Ponieważ jednak jest to strona dla programistów, postaram się zachować moją odpowiedź tak praktyczną, jak to możliwe (i naprawdę, typy są niezwykle praktyczne w programowaniu, pomimo tego, co niektórzy mogą myśleć).

Przegląd

Zacznijmy od siedzenia w spodniach, aby zrozumieć, do czego służy system typów, zanim przejdziemy do bardziej formalnych podstaw. System typów narzuca strukturę naszym programom . Mówią nam, jak możemy połączyć różne funkcje i wyrażenia razem. Bez struktury programy są nie do utrzymania i niezwykle złożone, gotowe do wyrządzenia szkody przy najmniejszym błędzie programisty.

Pisanie programów z układem typów jest jak prowadzenie samochodu w idealnym stanie - hamulce działają, drzwi zamykają się bezpiecznie, silnik jest naoliwiony itp. Pisanie programów bez układu typu jest jak jazda motocyklem bez kasku z wykonanymi kołami z spaghetti. Nie masz absolutnie żadnej kontroli nad sobą.

Uziemienie dyskusji załóżmy, że mamy język z dosłownej wypowiedzi num[n]i str[s]że reprezentuje liczebnik N i łańcuch s, odpowiednio, i prymitywne funkcje plusi concat, z zamierzonego znaczenia. Oczywiście nie chcesz być w stanie napisać czegoś takiego jak plus "hello" "world"lub concat 2 4. Ale jak możemy temu zapobiec? A priori nie ma metody odróżnienia cyfry 2 od dosłownego ciągu „świat”. Chcielibyśmy powiedzieć, że wyrażeń tych należy używać w różnych kontekstach; mają różne typy.

Języki i typy

Cofnijmy się nieco: czym jest język programowania? Ogólnie rzecz biorąc, możemy podzielić język programowania na dwie warstwy: składnię i semantykę. Są one również nazywane odpowiednio statyką i dynamiką . Okazuje się, że system typów jest niezbędny do pośredniczenia w interakcji między tymi dwiema częściami.

Składnia

Program jest drzewem. Nie daj się zwieść wierszom tekstu pisanym na komputerze; są to tylko czytelne dla człowieka reprezentacje programu. Sam program jest abstrakcyjnym drzewem składni . Na przykład w C możemy napisać:

int square(int x) { 
    return x * x;
 }

To jest konkretna składnia programu (fragment). Reprezentacja drzewa to:

     function square
     /     |       \
   int   int x    return
                     |
                   times
                  /    \
                 x      x

Język programowania dostarcza gramatyki określający aktualne drzew tego języka (zarówno składni abstrakcyjnej betonu lub mogą być używane). Zwykle odbywa się to za pomocą zapisu BNF. Zakładam, że zrobiłeś to dla języka, który stworzyłeś.

Semantyka

OK, wiemy, co to jest program, ale to tylko statyczna struktura drzewa. Przypuszczalnie chcemy, aby nasz program rzeczywiście coś obliczał . Potrzebujemy semantyki.

Semantyka języków programowania to bogata dziedzina nauki. Ogólnie rzecz biorąc, istnieją dwa podejścia: semantyka denotacyjna i semantyka operacyjna . Semantyka denotacyjna opisuje program, mapując go na pewną podstawową strukturę matematyczną (np. Liczby naturalne, funkcje ciągłe itp.). to nadaje sens naszemu programowi. Przeciwnie, semantyka operacyjna definiuje program, opisując szczegółowo jego wykonanie. Moim zdaniem semantyka operacyjna jest bardziej intuicyjna dla programistów (w tym mnie), więc trzymajmy się tego.

Nie będę omawiał, jak zdefiniować formalną semantykę operacyjną (szczegóły są nieco zaangażowane), ale w zasadzie chcemy zasad takich jak:

1. num[n] jest wartością
2. str[s] jest wartością
3. Jeśli num[n1]i num[n2]oceniamy na liczby całkowite n_1$ and $n_2$, thenplus (num [n1], num [n2]) `ocenia na liczbę całkowitą $ n_1 + n_2 $.
4. Jeśli str[s1]i analizuje str[s2]ciągi s1 i s2, to concat(str[s1], str[s2])ocenia na ciąg s1s2.

Itd. Zasady są w praktyce o wiele bardziej formalne, ale rozumiesz sedno. Jednak wkrótce mamy problem. Co się stanie, gdy napiszemy:

concat(num[5], str[hello])

Hm To dość zagadka. Nigdzie nie zdefiniowaliśmy reguły łączenia liczb z ciągiem znaków. Moglibyśmy spróbować stworzyć taką regułę, ale intuicyjnie wiemy, że ta operacja jest bez znaczenia. Nie chcemy, aby ten program był prawidłowy. W ten sposób jesteśmy nieuchronnie prowadzeni do typów.

Rodzaje

Program jest drzewem zdefiniowanym przez gramatykę języka. Programy mają znaczenie dzięki regułom wykonania. Ale niektórych programów nie można uruchomić; to znaczy, niektóre programy są bez znaczenia . Te programy są źle wpisane. W ten sposób pisanie charakteryzuje znaczące programy w języku. Jeśli program jest dobrze napisany, możemy go uruchomić.

Podajmy kilka przykładów. Ponownie, podobnie jak w przypadku reguł oceny, przedstawię reguły pisania nieformalnie, ale można je usztywnić. Oto kilka zasad:

1. Token formularza num[n]ma typ nat.
2. Token formularza str[s]ma typ str.
3. Jeśli wyrażenie e1ma typ, nata wyrażenie e2ma typ nat, to wyrażenie plus(e1, e2)ma typ nat.
4. Jeśli wyrażenie e1ma typ, stra wyrażenie e2ma typ str, to wyrażenie concat(e1, e2)ma typ str.

Zatem zgodnie z tymi regułami istnieje plus(num[5], num[2])typ nat, ale nie możemy przypisać typu do plus(num[5], str["hello"]). Mówimy, że program (lub wyrażenie) jest dobrze napisany, jeśli możemy przypisać mu dowolny typ, a w przeciwnym razie jest źle napisany. System typów jest poprawny, jeśli wszystkie dobrze napisane programy mogą zostać wykonane. Haskell jest zdrowy; C nie jest.

Wniosek

Istnieją inne poglądy na typy. Typy w pewnym sensie odpowiadają logice intuicyjnej i mogą być również postrzegane jako obiekty w teorii kategorii. Zrozumienie tych połączeń jest fascynujące, ale nie jest konieczne, jeśli ktoś chce tylko napisać lub nawet zaprojektować język programowania. Jednak zrozumienie typów jako narzędzia do kontrolowania formacji programów jest niezbędne do projektowania i rozwoju języka programowania. Podrapałem tylko powierzchnię tego, co typy mogą wyrazić. Mam nadzieję, że uważasz, że są one warte zachodu w Twoim języku.