Typ wymazywania jest dobry
Trzymajmy się faktów
Wiele dotychczasowych odpowiedzi jest nadmiernie zaniepokojonych użytkownikami Twittera. Warto skupić się na wiadomościach, a nie na posłańcu. Jest dość spójna wiadomość, zawierająca nawet tylko wspomniane dotąd fragmenty:
To zabawne, gdy użytkownicy Javy narzekają na wymazywanie typów, co jest jedyną rzeczą, którą Java zrobiła dobrze, ignorując wszystkie rzeczy, które popełniły błąd.
Dostaję ogromne korzyści (np. Parametryczność) i zerowy koszt (rzekomy koszt to granica wyobraźni).
nowy T to zepsuty program. Jest izomorficzne z twierdzeniem, że „wszystkie zdania są prawdziwe”. Nie jestem w tym duży.
Cel: rozsądne programy
Te tweety odzwierciedlają perspektywę, która nie jest zainteresowana tym, czy możemy zmusić maszynę do zrobienia czegoś , ale bardziej tym, czy możemy uzasadnić, że maszyna zrobi coś, czego naprawdę chcemy. Dobre rozumowanie jest tego dowodem. Dowody można określić za pomocą notacji formalnej lub mniej formalnej. Niezależnie od języka specyfikacji muszą być jasne i rygorystyczne. Nieformalne specyfikacje nie są niemożliwe do poprawnej struktury, ale często zawierają błędy w praktycznym programowaniu. W końcu otrzymujemy środki zaradcze, takie jak testy automatyczne i eksploracyjne, aby nadrobić problemy, które mamy z nieformalnym rozumowaniem. Nie oznacza to, że testowanie jest z natury złym pomysłem, ale cytowany użytkownik Twittera sugeruje, że istnieje znacznie lepszy sposób.
Dlatego naszym celem jest posiadanie poprawnych programów, co do których możemy jasno i rygorystycznie rozumować, w sposób odpowiadający temu, jak maszyna faktycznie wykona program. Nie jest to jednak jedyny cel. Chcemy również, aby nasza logika miała pewien stopień ekspresji. Na przykład, tylko tyle możemy wyrazić za pomocą logiki zdań. Fajnie jest mieć uniwersalną (∀) i egzystencjalną (∃) kwantyfikację z czegoś w rodzaju logiki pierwszego rzędu.
Używanie systemów typów do rozumowania
Te cele można bardzo dobrze rozwiązać za pomocą systemów typów. Jest to szczególnie jasne ze względu na korespondencję Curry-Howard . Tę zgodność często wyraża się następującą analogią: typy są do programów, tak jak twierdzenia do dowodów.
Ta korespondencja jest dość głęboka. Możemy przyjąć logiczne wyrażenia i przetłumaczyć je poprzez korespondencję na typy. Następnie, jeśli mamy program o tej samej sygnaturze typu, który kompiluje, udowodniliśmy, że wyrażenie logiczne jest uniwersalnie prawdziwe (tautologia). Dzieje się tak, ponieważ korespondencja jest dwukierunkowa. Transformacja między typem / programem a światami twierdzeń / dowodów jest mechaniczna iw wielu przypadkach może być zautomatyzowana.
Curry-Howard dobrze wpisuje się w to, co chcielibyśmy zrobić ze specyfikacjami programu.
Czy systemy typów są przydatne w Javie?
Nawet rozumiejąc Curry-Howard, niektórym osobom łatwo jest zlekceważyć wartość systemu czcionek, gdy
- jest niezwykle ciężka w pracy
- odpowiada (poprzez Curry-Howard) logice o ograniczonej ekspresji
- jest uszkodzony (co powoduje scharakteryzowanie systemów jako „słabe” lub „silne”).
Jeśli chodzi o pierwszy punkt, być może IDE sprawiają, że system typów Javy jest wystarczająco łatwy w obsłudze (to wysoce subiektywne).
Jeśli chodzi o drugi punkt, zdarza się, że Java prawie odpowiada logice pierwszego rzędu. Typy generyczne wykorzystują system typów równoważny uniwersalnej kwantyfikacji. Niestety, symbole wieloznaczne dają nam tylko niewielki ułamek kwantyfikacji egzystencjalnej. Ale uniwersalna kwantyfikacja to całkiem dobry początek. Fajnie jest móc powiedzieć, że funkcje List<A>
działają uniwersalnie dla wszystkich możliwych list, ponieważ A jest całkowicie nieograniczony. Prowadzi to do tego, o czym mówi użytkownik Twittera w odniesieniu do „parametryczności”.
Często cytowanym artykułem na temat parametryczności jest bezpłatne twierdzenie Philipa Wadlera ! . Interesujące w tym artykule jest to, że na podstawie samego podpisu typu możemy udowodnić kilka bardzo interesujących niezmienników. Gdybyśmy mieli napisać testy automatyczne dla tych niezmienników, marnowalibyśmy bardzo czas. Na przykład for List<A>
, z samego podpisu typu forflatten
<A> List<A> flatten(List<List<A>> nestedLists);
możemy to uzasadnić
flatten(nestedList.map(l -> l.map(any_function)))
≡ flatten(nestList).map(any_function)
To prosty przykład i prawdopodobnie możesz uzasadnić to nieformalnie, ale jest jeszcze ładniej, gdy otrzymamy takie dowody formalnie za darmo z systemu typów i sprawdzone przez kompilator.
Brak usunięcia może prowadzić do nadużyć
Z punktu widzenia implementacji języka, typy generyczne Javy (które odpowiadają typom uniwersalnym) wpływają bardzo mocno na parametryczność wykorzystywaną do uzyskiwania dowodów na to, co robią nasze programy. To prowadzi do trzeciego wspomnianego problemu. Wszystkie te zyski dowodu i poprawności wymagają systemu typu dźwiękowego zaimplementowanego bez wad. Java z pewnością ma pewne funkcje językowe, które pozwalają nam zniszczyć nasze rozumowanie. Należą do nich między innymi:
- skutki uboczne z systemem zewnętrznym
- odbicie
Nieusunięte rodzaje ogólne są pod wieloma względami powiązane z refleksją. Bez wymazywania istnieją informacje o czasie wykonywania, które są przenoszone z implementacją, których możemy użyć do zaprojektowania naszych algorytmów. Oznacza to, że statycznie, gdy wnioskujemy o programach, nie mamy pełnego obrazu. Odbicie poważnie zagraża poprawności wszelkich dowodów, o których wnioskujemy statycznie. To nie przypadek, że refleksja prowadzi również do różnych trudnych defektów.
Więc w jaki sposób nieusunięte typy generyczne mogą być „przydatne”? Rozważmy użycie wspomniane w tweecie:
<T> T broken { return new T(); }
Co się stanie, jeśli T nie ma konstruktora bez argonu? W niektórych językach otrzymujesz wartość zerową. A może pomijasz wartość null i przechodzisz od razu do zgłaszania wyjątku (do którego wartości null wydają się prowadzić). Ponieważ nasz język jest kompletny w Turingu, nie można wywnioskować, które wywołania broken
będą obejmować „bezpieczne” typy z konstruktorami bezargumentowymi, a które nie. Straciliśmy pewność, że nasz program działa uniwersalnie.
Wymazywanie oznacza, że uzasadniliśmy (więc wymażmy)
Jeśli więc chcemy uzasadniać nasze programy, stanowczo odradzamy stosowanie funkcji językowych, które silnie zagrażają naszemu rozumowaniu. Kiedy już to zrobimy, dlaczego nie po prostu porzucić typów w czasie wykonywania? Nie są potrzebne. Możemy uzyskać pewną wydajność i prostotę z satysfakcją, że żadne rzutowanie nie zawiedzie lub że podczas wywołania może brakować metod.
Wymazywanie zachęca do rozumowania.