Korzystasz z „silnego” systemu typu w prawdziwym świecie, powiedzmy, do dużych aplikacji internetowych?

Wiem, że jest to bardzo szerokie, dwuznaczne i być może filozoficzne pytanie. Do tego stopnia, że ​​najważniejsze słowo kluczowe w pytaniu - „silny” typ systemu - samo w sobie jest źle zdefiniowane . Pozwól mi więc wyjaśnić, co mam na myśli.

Ogólny kontekst pytania

W Ruby on Rails budowaliśmy bardzo dużą aplikację internetową i ogólnie jesteśmy zadowoleni z naszego stosu. Kiedy chcemy, możemy wysyłać rzeczy naprawdę szybko - coś, co działa w 90% przypadków „biznesowych”, nie martwiąc się zbytnio o 10% przypadków przewagi. Z drugiej strony, za pomocą recenzji kodu i pokrycia testowego możemy być powolni i celowi oraz upewnić się, że pokrywamy wszystkie bazy - ponownie, tylko w sytuacjach, które wymagają tak dokładniejszej kontroli i bezpieczeństwa.

Jednak wraz z powiększaniem się zespołu poczułem się nieswojo z powodu braku „siatki bezpieczeństwa” upieczonej na naszym stosie.

Niedawno rozpoczęliśmy prace nad rodzimym programowaniem Androida na Javie. I (przyjemnie) przypomniano mi o bezpieczeństwie zapewnianym przez skompilowany / statyczny / silnie napisany język.

• Błędne zmienne, niepoprawne typy danych, niepoprawne wywołania funkcji i wiele trywialnych błędów są przechwytywane przez twoje IDE. Wszystko dlatego, że IDE może podłączyć się do kompilatora i zweryfikować pewne aspekty „poprawności” programu.
• Chcesz zmienić podpis funkcji? Łatwy. Kompilator + IDE może pomóc w wykryciu WSZYSTKICH witryn wywołujących.
• Chcesz się upewnić, że pewne wyjątki są zawsze obsługiwane? Sprawdzone wyjątki na ratunek.

Teraz, chociaż te funkcje bezpieczeństwa mają swoje zalety, jestem również świadomy ich wad. Co więcej, w świecie „ciężkiego” Java. Dlatego zamiast Java zacząłem patrzeć na mnóstwo współczesnych, „silnie pisanych” języków, nad którymi ludzie zaczęli pracować w tych dniach. Na przykład: Scala, Rust, Haskell itp. Najbardziej interesuje mnie moc ich systemów typów i sprawdzanie czasu statycznego / kompilacji.

Teraz pytanie

Jak korzystać z tych potężnych systemów typu i funkcji statycznych / czas kompilacji w większych aplikacjach?

Na przykład, w jaki sposób mógłbym wyjść poza standardowy rodzaj „cześć świata”, wprowadzając te zaawansowane funkcje? Taki, który używa systemu typu bogatego do modelowania problemu w domenie biznesowej? Czy system typów pomaga, czy przeszkadza, gdy jesteś w strefie 30 000 LOC +? Co dzieje się z siatką bezpieczeństwa zapewnianą przez tego typu systemy (i kontrole czasu kompilacji), gdy Twój system wchodzi w interakcję ze słabo wpisanym światem zewnętrznym, np. poprzez interfejsy API JSON lub XML, różne magazyny danych, dane wejściowe użytkownika itp.

Dam krótką odpowiedź z powodu mojego braku czasu, ale obecnie pracuję nad dwoma dużymi projektami (> 100 000 LOC w Haskell) - flowbox.io i luna-lang.org. Używamy Haskell do wszystkich części, w tym backendu, kompilatora naszego języka programowania, a nawet GUI opartego na webGL. Muszę przyznać, że silny system pisma i maszyneria typu „zależnego” może cię poprowadzić i uchronić przed ciężarem i kłopotami znanymi z innych języków. Używamy typów bardzo szeroko i wszystko, co można sprawdzić w czasie kompilacji, jest zrobione. W rzeczywistości w ciągu ostatnich 3 lat rozwoju nigdy nie napotkaliśmy żadnego błędu środowiska uruchomieniowego ani przepełnienia stosu (i jest to coś naprawdę niesamowitego). Jedynymi błędami są oczywiste błędy logiczne popełniane przez programistów. Wiele osób mówi, że jeśli coś kompiluje się w Haskell, to po prostu działa i powinieneś być całkiem pewien, że któregoś dnia nie rozwali ci twarzy.

Odpowiadając na pierwszą część pytania: Możesz dowiedzieć się o tych potężnych funkcjach systemu typu, czytając kilka świetnych blogów, takich jak:

• Blog Bartosza Milewskiego
• Edwarda Kmetta
• lub Gabriel Gonzales jeden

W rzeczywistości istnieje wiele innych fajnych blogów (takich jak planeta Haskell ). W każdym razie najlepszym sposobem na prawdziwe zrozumienie zaawansowanych systemów typów jest opracowanie użytecznej biblioteki open source. My (w Flowbox i New Byte Order) wydajemy wiele bibliotek (można je znaleźć w Hackage), więc jeśli nie masz pojęcia, co rozwijać, zawsze możesz zaangażować się w nasze projekty - po prostu napisz do mnie chcieć (poczta dostępna na luna-lang.org ).

Pisanie słabe vs. mocne jest dość niejasno zdefiniowane. Co więcej, ponieważ najbliższym powszechnym zastosowaniem „silnego pisania” jest odwoływanie się do rzeczy, które utrudniają rzucanie typów, co nie pozostawia nic więcej do opisania jeszcze silniejszych systemów typów. To tak, jakby powiedzieć, że jeśli możesz unieść mniej niż 30 funtów, jesteś słaby, a każdy, kto może podnieść więcej, należy do tej samej kategorii „silnych” - mylące rozróżnienie.

Wolę więc definicję:

• Słabo typowane systemy używają typów, aby zapobiec robieniu pewnych rzeczy (np. Błędów)
• Silnie typowane systemy używają typów do robienia rzeczy za Ciebie

Co mam na myśli przez robienie rzeczy dla ciebie? Cóż, przeanalizujmy napisanie interfejsu API konwersji obrazu w ramach Servant (w Haskell, ale tak naprawdę nie musisz tego wiedzieć, aby zobaczyć, zobaczysz ...)

{-# LANGUAGE
    TypeOperators,
    DataKinds
    #-}

import Codec.Picture
import Data.Proxy
import Network.Wai.Handler.Warp (run)
import Servant
import Servant.JuicyPixels

main :: IO ()
main = run 8001 conversion

Oznacza to, że chcemy niektóre moduły, w tym pakiet Servant i wtyczkę JuicyPixels do Servant, oraz że głównym punktem wejścia programu jest uruchomienie funkcji „konwersji” na porcie 8001 jako serwer wykorzystujący backend Warp. Zignoruj ​​bit języka.

conversion :: Application
conversion = serve (Proxy :: Proxy ConversionApi) handler

Oznacza to, że funkcja konwersji to serwer, na którym interfejs API musi być zgodny z typem „ConversionApi”, a żądania są obsługiwane przez funkcję handler

type ConversionApi
     = ReqBody '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE] DynamicImage
    :> Post '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE] DynamicImage

Określa ConvesionApityp. Mówi, że powinniśmy akceptować typy treści przychodzących określone na liście „[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE] i traktować je jako DynamicImage oraz że powinniśmy zwrócić DynamicImage przekonwertowany na ten sam zakres treści typy. Nie martw się dokładnie o to, co:>, na razie pomyśl o tym jako o szczęśliwej magii.

Tak więc, biorąc pod uwagę moją preferowaną definicję, źle napisany system może teraz zapewnić takie rzeczy jak:

• Nie zwracasz niewłaściwego typu treści wychodzących
• Nie analizujesz przychodzącego żądania jako niewłaściwego typu treści
• Gdyby nasz serwer był bardziej skomplikowany, uniemożliwiłby nam to tworzenie zniekształconych identyfikatorów URI, ale tak naprawdę nie zwracamy żadnych stron HTML zawierających linki (a typ zapewnia, że ​​nie możemy!)
• Naprawdę ambitny system słabego pisania może nawet sprawdzić, czy wyczerpująco obsługujemy wszystkie przychodzące i wychodzące typy treści, pozwalając, aby ten typ działał również jako dokument specyfikacji, a nie tylko ograniczenie.

Wszystkie wzniosłe cele, ale w rzeczywistości niewystarczające do zakwalifikowania się jako system silnie typowy, biorąc pod uwagę powyższą definicję. A teraz musimy przejść do trudnej części pisania kodu zgodnego z tą specyfikacją. W naprawdę silnym systemie piszemy:

handler = return

A potem skończymy. To wszystko, nie ma już kodu do napisania . Jest to w pełni działający serwer WWW (modulo dowolne literówki, które przegapiłem). Ten typ powiedział kompilatorowi wszystko, czego potrzebuje do stworzenia naszego serwera WWW z typów i pakietów (technicznie modułów), które zdefiniowaliśmy i zaimportowaliśmy.

Jak więc nauczyć się tego robić na dużą skalę aplikacji? Cóż, tak naprawdę nie różni się zbytnio od używania ich w aplikacjach na mniejszą skalę. Typy absolutne nie dbają o to, ile kodu jest z nimi związane.

Kontrola typu wykonania jest prawdopodobnie rzeczą, której prawdopodobnie będziesz chciał uniknąć, ponieważ pochłania to ogromną korzyść i pozwala typom na skomplikowanie pracy nad projektem, a nie na uproszczenie typów.

Jako taki, jest to głównie kwestia praktyki modelowania rzeczy z typami. Dwa główne sposoby modelowania rzeczy (lub ogólnie budowania rzeczy) to oddolne i odgórne. Z góry na dół zaczyna się od najwyższego poziomu operacji, a podczas budowania modelu masz części, w których odkładasz modelowanie na później. Modelowanie oddolne oznacza, że ​​zaczynasz od operacji podstawowych, tak jak zaczynasz od funkcji podstawowych, a następnie budujesz coraz większe modele, aż w pełni uchwycisz działanie projektu. Od dołu do góry jest bardziej konkretny i prawdopodobnie szybciej się buduje, ale z góry na dół może lepiej poinformować modele niższego poziomu o tym, jak muszą się właściwie zachowywać.

Rodzaje są to, w jaki sposób programy odnoszą się do matematyki, dosłownie, więc tak naprawdę nie ma górnej granicy tego, jak skomplikowane mogą być, ani punkt, w którym można „zrobić” naukę o nich. Praktycznie wszystkie zasoby poza kursami uniwersyteckimi wyższego poziomu są poświęcone temu, jak typy działają w określonym języku, więc musisz o tym również zadecydować.

Jak najlepiej mogę zaoferować, typy można rozwarstwiać w następujący sposób:

• Bardzo słabo wpisane, takie jak JavaScript, w którym zdefiniowano [] + {}
• Słabo wpisane jak Python, gdzie nie możesz zrobić [] + {}, ale nie jest to sprawdzane, dopóki nie spróbujesz
• Słabo wpisane, jak C lub Java, gdzie nie możesz zrobić [] + {}, ale jest to sprawdzane podczas kompilacji, jednak nie masz bardziej zaawansowanych funkcji typu
• Wokół granicy między słabo i mocno wpisanymi, takimi jak metaprogramowanie szablonu C ++, i prostszy kod Haskell, w którym typy wymuszają tylko właściwości.
• W pełni w mocno wpisanych, takich jak bardziej skomplikowane programy Haskell, w których typy wykonują różne czynności, jak pokazano powyżej
• Bardzo silnie typowane, jak Agda lub Idris, gdzie typy i wartości oddziałują na siebie i mogą się wzajemnie ograniczać. Jest to tak silne, jak tylko systemy typów, a programowanie w nich jest takie samo jak pisanie matematycznych dowodów na to, co robi twój program. Uwaga: kodowanie w Agda nie jest dosłownie pisząc dowodów matematycznych, typy są teorie matematyczne i funkcje z tych typów są konstruktywne przykłady potwierdzające te teorie.

Ogólnie rzecz biorąc, im niżej znajdujesz się na liście, tym więcej typów mogą dla Ciebie zrobić, ale na samym dole wspinasz się w stratosferę, a powietrze staje się nieco rzadkie - ekosystem opakowań jest znacznie mniejszy, a Ty ' Będę musiał sam napisać więcej rzeczy niż znaleźć odpowiednią bibliotekę. Bariera wejścia również rośnie wraz ze spadkiem, ponieważ musisz właściwie zrozumieć system typów wystarczający do pisania programów na dużą skalę.

Właśnie zacząłem pracować nad głównym zespołem dużej platformy napisanej w Scali. Możesz spojrzeć na udane aplikacje typu open source, takie jak Scalatra, Play lub Slick, aby zobaczyć, jak radzą sobie z niektórymi bardziej szczegółowymi pytaniami dotyczącymi interakcji z dynamicznymi formatami danych.

Jedną z największych zalet silnego pisania Scali, jaką odkryliśmy, jest edukacja użytkowników. Zespół podstawowy może podejmować decyzje i egzekwować je w systemie typów, więc gdy inne zespoły, które są znacznie mniej obeznane z zasadami projektowania, muszą wchodzić w interakcje z systemem, kompilator je koryguje, a zespół podstawowy nie dokonuje ciągłych poprawek wyciągnij wnioski. To ogromna zaleta w dużym systemie.

Oczywiście nie wszystkie zasady projektowania można egzekwować w systemie typów, ale im silniejszy system typów, tym więcej zasad projektowania można egzekwować w kompilatorze.

Możemy również ułatwić użytkownikom. Często dla nich po prostu pracują ze zwykłymi kolekcjami lub klasami spraw, a my konwertujemy je na JSON lub cokolwiek automatycznie, gdy jest to potrzebne do transportu sieciowego.

Silne pisanie pomaga również rozróżniać takie rzeczy, jak wprowadzanie danych niezarządzanych i oczyszczonych, co może pomóc w bezpieczeństwie.

Silne pisanie pomaga także w większym skupieniu się na twoich faktycznych zachowaniach , zamiast konieczności testowania wielu testów. Sprawia, że ​​testowanie jest znacznie przyjemniejsze, bardziej skoncentrowane, a zatem bardziej skuteczne.

Główną wadą jest nieznajomość języka i paradygmatu językowego, który można naprawić z czasem. Poza tym uznaliśmy, że jest to warte wysiłku.

Chociaż nie jest to bezpośrednia odpowiedź (ponieważ nie pracowałem jeszcze na +30 000 baz kodu LOC w haskell :( ..), proszę o sprawdzenie https://www.fpcomplete.com/business/resources/case-studies / który zawiera wiele analiz przypadków haskell w rzeczywistych ustawieniach branżowych.

Kolejnym dobrym artykułem jest IMVU, które opisują swoje doświadczenia zmieniające się w haskell - http://engineering.imvu.com/2014/03/24/what-its-like-to-use-haskell/ .

Z własnego doświadczenia w większych aplikacjach system typów bardzo ci pomaga, zwłaszcza jeśli próbujesz zakodować jak najwięcej typów. Prawdziwa moc jest naprawdę oczywista, jeśli chodzi o refaktoryzację rzeczy - co oznacza utrzymanie i takie stają się znacznie mniej niepokojącym zadaniem.

Zrzucę kilka linków do zalecanych zasobów, ponieważ zadajesz sporo pytań na raz:

• Małe serie na temat popularnych optymalizacji w haskell
• Myślenie typami
• Ponieważ jesteś w świecie deweloperów internetowych, sugeruję sprawdzenie Yesod , który jest jednym z niesamowitych frameworków internetowych w haskell (oferuje trasy bezpieczne dla typu i wiele więcej).

Na zakończenie uwaga dotycząca radzenia sobie ze światem zewnętrznym odbywa się na kilka sposobów. Istnieją biblioteki, które zapewniają bezpieczeństwo typów, takie jak Aeson dla JSON, Esqueleto dla SQL i wiele innych.

Co widziałem:

Pracowałem nad kilkoma dużymi aplikacjami Ruby (Rails), jedną dużą aplikacją Haskell i kilkoma mniejszymi. Dzięki temu doświadczeniu muszę powiedzieć, że życie w aplikacjach Haskell jest o wiele łatwiejsze niż w Railsach, jeśli chodzi o konserwację i niższą krzywą uczenia. Uważam, że korzyści te wynikają zarówno z systemu typów Haskella, jak i funkcjonalnego stylu programowania. Jednak, w przeciwieństwie do wielu, uważam, że „statyczna” część systemu typów jest po prostu ogromną wygodą, ponieważ nadal można korzystać z dynamicznych kontraktów.

To, w co wierzę

Jest ładny pakiet o nazwie Kontrakty Rubin, który idzie w parze z dostarczaniem niektórych głównych funkcji, które, jak sądzę, pomagają projektom Haskell osiągnąć lepszą charakterystykę konserwacji. Kontrakty Ruby przeprowadza kontrole w czasie wykonywania, więc najlepiej jest, gdy jest połączone z wysokim testem zbieżności, ale nadal zapewnia tę samą wewnętrzną dokumentację i wyrażenie intencji i znaczenia, jak przy użyciu adnotacji typu w językach takich jak Haskell.

Odpowiedź na pytanie

Aby odpowiedzieć na powyższe pytania, istnieje wiele miejsc, w których można zapoznać się z Haskell i innymi językami z zaawansowanymi systemami typów. Jednak, szczerze mówiąc, chociaż te źródła dokumentacji są doskonałe same w sobie, wszystkie wydają się nieco rozczarowujące w porównaniu z mnóstwem dokumentacji i praktycznych porad w Ruby, Python, Java i innych takich językach. W każdym razie Real World Haskell się starzeje, ale nadal jest dobrym źródłem.

Teoria kategorii

Jeśli wybierzesz Haskell, napotkasz dużą ilość literatury na temat teorii kategorii. Teoria kategorii IMHO jest przydatna, ale nie konieczna. Biorąc pod uwagę rozpowszechnienie w społeczności Haskell, łatwo jest powiązać wady i zalety typów z odczuciami na temat praktyczności teorii kategorii. Warto pamiętać, że są to dwie różne rzeczy, to znaczy, że implementacje kierowane przez teorię kategorii mogą być wykonywane zarówno w językach dynamicznie typowanych, jak i statycznych (modulo korzyści, jakie zapewnia system typów). Zaawansowane systemy typów zasadniczo nie są powiązane z teorią kategorii, a teoria kategorii nie jest związana z systemami typów.

Więcej na temat typów

Kiedy dowiesz się więcej o programowaniu za pomocą typów i technik w nim zawartych (co dzieje się dość szybko, ponieważ jest fajnie), będziesz chciał wyrazić więcej za pomocą systemu typów. W takim przypadku przejrzałbym niektóre z poniższych zasobów i przyłączył się do mnie, aby uświadomić sprzedawcom narzędzi, że chcemy narzędzi jakości przemysłowej z tymi funkcjami tylko w coś, co ujawnia łatwy w użyciu interfejs (np. Kontrakty Ruby):

• Wprowadzenie do programowania w ATS

• Typy udoskonalania LiquidHaskell za pośrednictwem SMT i abstrakcji predykatów

• Rozwój oparty na typach dzięki Idris

Po pierwsze, czuję, że istnieje pomieszanie w odpowiedziach między słabo wpisanym a silnie wpisanym, a statycznym i dynamicznym. Link pod warunkiem, że podany OP wyraźnie odróżnia:

Silny system typów to system typów, który ma ograniczenie czasu kompilacji lub funkcję czasu wykonywania, które uważasz za atrakcyjne.

Słaby system typów to system typów pozbawiony tego ograniczenia lub cechy.

Na przykład C, C ++ i Java są wpisywane statycznie, ponieważ zmienne są wpisywane w czasie kompilacji. Jednak C i C ++ można uznać za słabo wpisane, ponieważ język pozwala na ominięcie ograniczeń za pomocą void *wskaźników i rzutowań. Więcej na ten temat.

W tym rozróżnieniu mocne pisanie może być tylko lepsze. Im wcześniej porażka, tym lepiej.

Jednak przy pisaniu dużych programów nie sądzę, aby system pisma odgrywał ważną rolę. Jądro Linuksa ma dziesięć milionów LOC napisanych w C i asemblerze i jest uważane za bardzo stabilny program, jest daleko od moich 200 linii Java, które prawdopodobnie są pełne luk bezpieczeństwa. Podobnie, chociaż dynamicznie wpisywane „języki skryptowe” mają złą reputację, jeśli chodzi o pisanie dużych programów, czasami istnieje dowód, że jest niezasłużony (np. Python Django, ponad 70 000 LOC)

Moim zdaniem chodzi o standard jakości. Odpowiedzialność za skalowalność dużych aplikacji powinny ponosić wyłącznie programiści i architekci oraz ich wola, aby aplikacja była czysta, przetestowana, dobrze udokumentowana itp.

Gdzie można przeczytać o tym, jak korzystać z tych potężnych systemów typu i funkcji statycznych / czas kompilacji w większych aplikacjach?

z poprzedniej odpowiedzi https://www.fpcomplete.com/business/resources/case-studies/

W jaki sposób można wyjść poza standardowe wprowadzenie do tych potężnych funkcji „witaj świecie”?

tak naprawdę jak każdy inny język buduje siłę

W jaki sposób można użyć systemu typu bogatego do modelowania problemu domeny biznesowej?

Za pomocą abstrakcyjnych typów danych lub bardziej ogólnie polimorfizmu

Czy system typów pomaga, czy przeszkadza, gdy jesteś w strefie 30 000 LOC +?

Pomaga przez całą drogę. system typów pomaga pisać kod, ponieważ określa kształt wyniku, jaki chcesz uzyskać. Właściwie Agda pisze dla ciebie kod.

PS: nie popełniaj błędu posiadania systemu typów i samodzielnego pisania typów, co jest idiotyczne: komputer może to zrobić za Ciebie.

Co dzieje się z siatką bezpieczeństwa zapewnianą przez tego typu systemy (i kontrole czasu kompilacji), gdy Twój system wchodzi w interakcję ze słabo wpisanym światem zewnętrznym, np. poprzez interfejsy API JSON lub XML, różne magazyny danych, dane wejściowe użytkownika itp.

To wspaniale, ponieważ znajomość struktury wartości według typów oznacza, że ​​komputer może zaproponować ci sposób napisania (de) serializatora.

Jeśli naprawdę chcesz wiedzieć o typach i abstrakcji, najlepszym wprowadzeniem jest temat Zrozumienie typów, abstrakcja danych i polimorfizm

To papier, nie studium przypadku z ładnymi zdjęciami, ale jest pouczające

Jako programista .net, który dużo pracuje na aplikacjach internetowych, widzę zarówno wpisane C #, jak i nietypowe strony Javascript.

Nie jestem pewien, czy widziałem literaturę dotyczącą zadawanych pytań. Używając języka pisanego, bierzesz to wszystko za pewnik. W przypadku typu bez typu zobaczysz, że definiowanie typów jest niepotrzebnym narzutem.

Osobiście nie sądzę, abyś mógł zaprzeczyć, że mocno napisany język oferuje korzyści, które opisujesz przy bardzo niskim koszcie (w porównaniu do pisania równoważnych testów jednostkowych). Interakcja ze słabo typowanymi systemami zwykle obejmuje typy ogólne, takie jak tablice lub słowniki obiektów, takie jak DataReader, lub kreatywne użycie ciągu znaków lub nowej klasy dynamicznej. Zasadniczo wszystko działa, po prostu pojawia się błąd czasu wykonania zamiast czasu kompilacji.

Jeśli chcesz napisać bardzo krótki program, być może definiujący funkcję w kilku liniach do pracy z większą aplikacją, po prostu nie masz miejsca na deklarowanie klas. Z pewnością jest to niszowa, nietypowa wersja językowa, taka jak JS?