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

29

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.

Saurabh Nanda
źródło
12
To nie na temat, ponieważ nie ma prawdziwej odpowiedzi. Pytanie ma sprowokować dyskusyjną dyskusję („Lubię / nie lubię typów statycznych, ponieważ ...”), a nie faktyczne wyjaśnienie . Radzę wybrać jedną z bardziej szczegółowych części twojego pytania, na przykład: „Co stanie się z siatką bezpieczeństwa zapewnianą przez te systemy typu, gdy twój system wchodzi w interakcję ze słabo wpisanym światem zewnętrznym?” i przepisz pytanie, aby o tym mówić. Otrzymasz ostateczne odpowiedzi, które będą przydatne dla przyszłych czytelników.
Benjamin Hodgson,
5
Zalecenia dotyczące zasobów również są tutaj nie na temat (ponieważ takie odpowiedzi szybko się zmieniają i naprawdę nie jesteśmy lepsi od Google). Jak powiedział Benjamin, w twoim poście są ukryte pytania, na które można odpowiedzieć, ale cały post w obecnym stanie zasadniczo prosi ludzi o opisanie swoich doświadczeń za pomocą tych języków, co jest o wiele lepiej dostosowane do Quora lub Reddit niż StackExchange teren. Nie oddaję głosu, ponieważ to pytanie jest dobrze zadawane, ale nie jest to pytanie StackExchange.
Ixrec,
4
System typów jest narzędziem i jak każde inne narzędzie, jego skuteczność zależy w dużej mierze nie od samego narzędzia, ale od posiadacza. Możesz wykorzystać system typów języka takiego jak Haskell, aby zakodować niezmienniki dotyczące logiki biznesowej na poziomie typu i zlecić sprawdzenie tych niezmienników przez maszynę (kompilator) w czasie kompilatora, ale aby to zrobić, musisz zrozumieć semantykę system typów i sprawdzanie typu. Właściwe pytanie nie brzmi „czy to dobre narzędzie do tworzenia stron internetowych”, ale „oto kilka konkretnych problemów, z którymi się borykam; w jaki sposób można użyć silnego systemu typów do ich rozwiązania?”
user2407038,
5
Większość opisywanych rzeczy nie ma nic wspólnego z systemem typów. Są to funkcje wyłącznie IDE. Z wyjątkiem (bez zamiaru słów) sprawdzonych wyjątków, wszystkie wymienione przez ciebie funkcje były obecne w IDE Smalltalk na długo przed pojawieniem się w IDE dla języków o typie statycznym. W rzeczywistości jeden z najczęściej używanych IDE Java faktycznie zaczął jako zmodyfikowany SmallEalk IDE (IBM VisualAge Smalltalk, który został zmodyfikowany w celu zrozumienia kodu Java, ale nadal był napisany w Smalltalk i wydany jako VisualAge Java, który został następnie przeniesiony na Javę i wydany jako…
Jörg W Mittag,
4
… VisualAge Java Micro Edition, która została następnie podzielona na komponenty wielokrotnego użytku i wydana jako Open Source pod nazwą Eclipse). Jak na ironię w kontekście tego pytania, właśnie dzięki dynamicznej naturze systemów Smalltalk, IDE Smalltalk są tak potężne. Na przykład wymyślono zautomatyzowane refaktoryzacje i po raz pierwszy wdrożono je w Smalltalk. Zgodnie z twoją logiką, Haskell musi mieć najlepsze IDE, ponieważ ma najsilniejszy, najostrzejszy system typów statycznych ze wszystkich wspomnianych języków. Ale tak nie jest. Wspomniałeś także o „podłączeniu się do kompilatora”. To ma…
Jörg W Mittag,

Odpowiedzi:

34

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:

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 ).

danilo2
źródło
4
„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 pewnego dnia nie rozwali ci twarzy.”: Użyłem Haskell tylko do małych (choć niebanalnych) projektów , ale mogę to potwierdzić: gdy kompilator Haskell jest zadowolony, rzadko znajduję błędy.
Giorgio,
1
Jestem prawdopodobnie jednym z „Haskellów”, którzy najbardziej nie znoszą typów (w końcu napisałem własną wersję Haskell bez typów ) - ale z różnych powodów większość ludzi tak robi. Jeśli chodzi o inżynierię oprogramowania, ja również mam wrażenie, że gdy GHC jest szczęśliwy, twój program po prostu działa. Systemy typu Haskell są doskonałym narzędziem nie tylko do wykrywania ludzkich błędów w programowaniu, ale także do kontrolowania ogromnych baz kodu. (Zawsze pamiętam uzasadnienie Giovanniego dla zbroi Mewtwo, ilekroć muszę naprawić błędy typu).
MaiaVictor
Blog Gabriela Gonzalesa najlepiej zacząć od.
sam boosalis
@ danilo2 Wysłałem wiadomość e-mail na adres contact @ w witrynie firmy. Poproś o odpowiedź. Dzięki!
Saurabh Nanda,
@SaurabhNanda: Sprawdziłem dwukrotnie naszą skrzynkę odbiorczą i nie widzę żadnej wiadomości od ciebie. Czy wysłałeś go na adres <at> luna-lang.org? Proszę o kontakt bezpośrednio, pisząc do mojego wojciech <dot> danilo <at> gmail <dot> com, a my zbadamy, co było przyczyną tego problemu :)
danilo2
17

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ę.

Steven Armstrong
źródło
Zauważ, że nie musisz poprzedzać listy na poziomie typu apostrofem, jeśli na liście znajduje się więcej niż element. Apostrof jest konieczny tylko w przypadku list na poziomie typu 0- lub 1-elementowych, ponieważ są one niejednoznaczne (mogą odnosić się do zwykłego konstruktora typu listy)
Gabriel Gonzalez,
1
Wiem, ale miałem wrażenie, że apostrof był po prostu dobrą formą dla ogólnie promowanych typów danych. EG to Proxy :: Proxy Truedziała, ale lepiej napisać to jako Proxy :: Proxy 'True.
Steven Armstrong,
1
Wydaje się, że lepiej nie zawijać różnych osi, według których można klasyfikować systemy typów. Kostka lambda Barendregta zawiera już trzy, a dodatkowo wzdłuż pojedynczej słabo-silnej osi zawiera się również statyczny vs. dynamiczny i parametryczny vs. polimorfizm ad hoc (ten ostatni pozwala technikowi służącemu na tworzenie typów wykonywać większą część „pracy” ”).
user2141650,
1
To prawda, ale odpowiedź jest już bardzo długa i musisz być na dobrej drodze do studiowania teorii typów, zanim kostka lambda naprawdę zacznie mieć sens. Co więcej, poza bardzo niszowymi (a ponieważ już włączam Haskell, a nawet Agdą, naprawdę mam na myśli dość niszowe) języki, tak naprawdę nie znajdziesz języka, który ma na przykład typy zależne, ale nie ma operatorów typów .
Steven Armstrong,
Czy potrafisz krótko wyjaśnić '[xs]składnię? To oczywiście nie jest Char, ale nie widzę w jaki sposób albo TypeOperatorsczy DataKindsumożliwia składnię alternatywną. Czy to jakieś quasi-cytowanie?
wchargin
10

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.

Karl Bielefeldt
źródło
8

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:

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.

Tehnix
źródło
1
dzięki za odpowiedź studia przypadków na fpcomplete.com/business/resources/case-studies nie są już dostępne.
Saurabh Nanda
Wygląda na to, że studia przypadków przeniesiono na fpcomplete.com/case-study
Steven Shaw
3

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):

Eric
źródło
2

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.

Arthur Havlicek
źródło
-1

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

Nicolas
źródło
-2

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?

Ewan
źródło
Masz na myśli wpisywanie / bez wpisywania lub pisanie statyczne / wpisywanie dynamiczne? JavaScript nie jest bez typu, ale dynamicznie.
Giorgio,
2
nie musisz definiować typów. każdy przyzwoity język wywnioskuje dla ciebie typy: haskell, ocaml, sml, F # ...
nicolas
1
kiedy jesteś przyzwyczajony do silnie typowanego języka, wszystko inne jest bez typu, kiedy mówię, zdefiniuj typy, mam na myśli „utwórz klasy”, z pewnością możesz użyć var ​​lub cokolwiek, ale to tylko sztuczka kompilatora
Ewan