Co to jest system typów?

50

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?

Mael
źródło
19
Kiedy ludzie mówią o systemach typów, zwykle mówią o pisaniu statycznym. Pisanie dynamiczne nie jest zbyt interesujące dla osób dbających o systemy typów, ponieważ gwarantuje prawie nic. Np. Jaką wartość może mieć zmienna x? Byle co.
Doval
7
Byłbym ciekawy, co mieli do powiedzenia, aby bronić / wyjaśnić swoją reakcję.
Newtopian
18
@Doval Dynamiczne pisanie może zagwarantować, że nie wejdziesz w nonsensowny stan, robiąc coś takiego jak dodanie 5 do swojego kota. Jasne, nie powstrzyma cię to przed próbowaniem , ale może przynajmniej powstrzymać to, co się naprawdę wydarzy, i da ci szansę dowiedzieć się, co poszło nie tak, i podjąć działania naprawcze, czego nie potrafi prawdziwie pozbawiony języka język.
8bittree
10
Ta osoba miała problem z odpowiedzią na „A jak typ jest przypisany do wartości?”. Chcieli usłyszeć o regułach pisania, a nie o schematach „ramka i wskaźnik”. Jednak śmiech był absolutnie niegrzeczny.
ogrodnik
10
Śmiejąca się osoba najprawdopodobniej jest fanatką jakiegoś konkretnego języka (rodziny) z silnym systemem typów (Haskell wydaje się popularny) i wyśmiewałaby wszystko, co jest mniej silne (a tym samym zabawkę) niż to, lub mocniejsze (i dlatego niepraktyczne), lub po prostu inny. Udział w dyskusji z fanatykami jest niebezpieczny i daremny. Takie śmiech jest tak niegrzeczny, że wskazuje na tego rodzaju głębsze problemy. Masz szczęście, że nie zaczęli głosić ...
hyde

Odpowiedzi:

30

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.

Telastyn
źródło
3
„W zależności od środowiska osoba ta mogła chcieć większego formalizmu w systemie typów”. To pewnie to. Nie koncentrowałem się na tym, co mogę udowodnić za pomocą systemu typów, ale raczej myślałem o tym jako o narzędziu. Dzięki za rekomendację książki!
Mael
1
@Mael Niektóre systemy typu są używane jako logika (patrz ramy logiczne ). więc w zasadzie typ podaje formuły, a programy są dowodami tych formuł (np. typ funkcji a -> bmoże być postrzegany jako implikujący b , tj. jeśli podasz mi wartość typu a, mogę uzyskać wartość typu b). Jednak aby było to spójne, język musi być całkowity, a zatem nie Turinga kompletny. Tak więc wszystkie systemy typu rzeczywistego faktycznie definiują niespójną logikę.
Bakuriu
20

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.

Erik Eidt
źródło
Nie sądzę, że tak zwane systemy hybrydowe są w ogóle bardzo powszechne. Jakie języki masz na myśli?
ogrodnik
2
@gardenhead, zdolność downcastu nie jest funkcją systemu typu statycznego, dlatego zwykle jest sprawdzana dynamicznie w czasie wykonywania.
Erik Eidt
1
@gardenhead: większość języków o typie statycznym pozwala na odroczenie pisania w środowisku wykonawczym, czy to po prostu za pomocą void *wskaźników C (bardzo słabych), obiektów dynamicznych C #, czy też istniejących ilościowo GADT Haskella (co daje raczej silniejsze gwarancje niż statycznie wpisane wartości w większości innych Języki).
leftaroundabout
To prawda, że ​​zapomniałem o „castingu”. Ale rzucanie jest tylko kulą dla systemu słabego typu.
ogrodnik
@gardenhead Oprócz języków statycznych zapewniających opcje dynamiczne, wiele języków dynamicznych zapewnia pewne pisanie statyczne. Na przykład Dart, Python i Hack, wszystkie mają tryby lub narzędzia do przeprowadzania analizy statycznej w oparciu o koncepcję „stopniowego pisania”.
IMSoP
14

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.

ogrodnik
źródło
4
+1. Największą sztuczką, jaką kiedykolwiek ciągnęli entuzjaści pisania dynamicznego, było przekonanie świata, że ​​można mieć „typy” bez systemu typów. :-)
ruakh
1
Ponieważ nie można automatycznie zweryfikować niczego interesującego dla dowolnych programów, każdy system typów musi zapewniać operatora rzutowania (lub odpowiednik moralny), albo poświęca kompletność Turinga. Dotyczy to oczywiście Haskell .
Kevin
1
@Kevin Zdaję sobie sprawę z twierdzenia Rice'a, ale nie jest ono tak istotne, jak mogłoby się wydawać. Na początek znaczna większość programów nie wymaga nieograniczonej rekursji. Jeśli pracujemy w języku, który ma tylko prymitywną rekurencję, takim jak Godel's System T, wówczas możemy zweryfikować interesujące właściwości za pomocą systemu typów, w tym zatrzymania. Większość programów w prawdziwym świecie jest raczej prosta - nie mogę myśleć o ostatnim czasie, kiedy naprawdę potrzebowałem castingu. Kompletność Turinga jest przereklamowana.
ogrodnik
9
„Pisanie dynamiczne nie jest tak naprawdę pisaniem” zawsze wydawało mi się, że muzycy klasyczni mówią „muzyka pop nie jest tak naprawdę muzyką”, ani ewangelicy, którzy mówią „katolicy nie są tak naprawdę chrześcijanami”. Tak, systemy typu statycznego są potężne, fascynujące i ważne, a dynamiczne pisanie jest czymś innym. Ale (jak opisują inne odpowiedzi) istnieje szereg przydatnych rzeczy poza statycznymi typami systemów, które tradycyjnie nazywane są pisaniem i które mają wspólne ważne cechy. Dlaczego trzeba nalegać, aby nasz rodzaj pisania był jedynym prawdziwym pisaniem?
Peter LeFanu Lumsdaine
5
@IMSoP: dla czegoś krótszego niż książka esej Chrisa Smitha Co warto wiedzieć przed debatą na temat systemów typów, jest świetne, wyjaśniając, dlaczego dynamiczne pisanie naprawdę różni się od pisania statycznego.
Peter LeFanu Lumsdaine