Czy teoria kategorii jest przydatna do nauki programowania funkcjonalnego?

Uczę się języka Haskell i fascynuje mnie język. Nie mam jednak żadnego poważnego doświadczenia matematycznego ani CS. Ale jestem doświadczonym programistą.

Chcę nauczyć się teorii kategorii, abym mógł stać się lepszy w Haskell.

Których tematów z teorii kategorii powinienem nauczyć się zapewniać dobrą podstawę do zrozumienia Haskell?

W poprzedniej odpowiedzi na stronie Theoretical Computer Science powiedziałem, że teoria kategorii jest „podstawą” teorii typów. Tutaj chciałbym powiedzieć coś mocniejszego. Teoria kategorii to teoria typów . I odwrotnie, teoria typów jest teorią kategorii . Pozwól mi rozwinąć te kwestie.

Teoria kategorii to teoria typów

$f : A \to B$$A$$B$$f$

$A$$B$$f$

Teoria typów to teoria kategorii

Przez „teorię typów” rozumiem dowolny formalny język pisany na maszynie, oparty na sztywnych regułach formowania terminów, które zapewniają, że wszystko sprawdza typ. Okazuje się, że ilekroć pracujemy w takim języku, pracujemy w strukturze teoretycznej. Nawet jeśli używamy notacji teoretycznych i myślimy teoretycznie, to ostatecznie piszemy rzeczy, które mają sens kategorycznie. To niesamowity fakt .

Historycznie Dana Scott mogła być pierwszą, która to zauważyła. Pracował nad produkcją modeli semantycznych języków programowania na podstawie typowego (i nietypowego) rachunku lambda. Tradycyjne modele teoretyczne nie były odpowiednie do tego celu, ponieważ języki programowania wiążą się z nieograniczoną rekurencją, której brakuje w teorii. Scott wynalazł serię modeli semantycznych, które uchwyciły zjawiska programowania i doszedł do wniosku, że typowany rachunek lambda dokładnie reprezentuje klasę zwaną kartezjańską kategorią zamkniętą . Istnieje wiele kartezjańskich zamkniętych kategorii, które nie są „teoretyczne”. Ale wpisany rachunek lambda stosuje się do nich wszystkich jednakowo. Scott napisał fajny esej zatytułowany „ Powiązane teorie rachunku lambda„wyjaśniając, co się dzieje, a niektóre z nich wydają się być dostępne w Internecie. Oryginalny artykuł został opublikowany w tomie zatytułowanym„ Do HB Curry: eseje na temat logiki kombinowanej, rachunku lambda i formalizmu ”, Academic Press, 1980. Berry i Curien doszedł do tej samej realizacji, prawdopodobnie niezależnie. Zdefiniowali kategoryczną abstrakcyjną maszynę (CAM) do wykorzystania tych pomysłów w implementacji języków funkcjonalnych, a język, który zaimplementowali, nazwano „CAML”, który stanowi podstawę F # Microsoftu .

$\times$$\to$$List$właśnie w celu sformalizowania koncepcji funkcji polimorficznych. Nazwali je „naturalnymi transformacjami”, „naturalnymi”, ponieważ są jedynymi, które można pisać w sposób poprawny dla typu, używając zmiennych typu. Można więc powiedzieć, że teoria kategorii została wymyślona właśnie w celu sformalizowania polimorficznych języków programowania, jeszcze zanim powstały języki programowania!

Tradycjonalista z zestawu teorii nie ma wiedzy o funktorach i naturalnych przekształceniach zachodzących pod powierzchnią, gdy używa notacji z zestawu teorii. Ale tak długo, jak wiernie używa systemu czcionek, tak naprawdę robi konstrukcje kategoryczne, nie będąc ich świadomym.

Wszystko powiedziane i zrobione, teoria kategorii jest kwintesencją matematycznej teorii typów i funkcji. Wszyscy programiści mogą więc skorzystać z nauki teorii kategorii, szczególnie programiści funkcjonalni. Niestety wydaje się, że nie ma żadnych podręczników dotyczących teorii kategorii skierowanych specjalnie do programistów. Książki „teoria kategorii dla informatyki” są zazwyczaj skierowane do studentów / badaczy informatyki teoretycznej. Książka Benjamina Pierce'a, Podstawowa teoria kategorii dla informatyków jest chyba najbardziej czytelna z nich.

Istnieje jednak wiele zasobów w sieci, które są przeznaczone dla programistów. Strona Haskellwiki może być dobrym punktem wyjścia. W Midlands Graduate School prowadzimy wykłady z teorii kategorii (między innymi). Kurs Grahama Huttona został ustalony jako kurs „dla początkujących”, a mój jako kurs „zaawansowany”. Ale oba obejmują zasadniczo tę samą treść, przechodząc do różnych głębokości. University of Chalmers ma ładną stronę z zasobami na temat książek i notatek z wykładów z całego świata. Entuzjastyczny site blog „SIGFPE” zapewnia również wiele dobrych przeczuć z punktu widzenia programisty.

Podstawowe tematy, których chcesz się nauczyć, to:

• definicja kategorii i kilka przykładów kategorii
• funktory i ich przykłady
• naturalne transformacje i ich przykłady
• definicje produktów, koproduktów i wykładników (przestrzenie funkcji), obiektów początkowych i końcowych.
• adiunkcje
• kategorie monady, algebry i Kleisli

Moje notatki z wykładów w Midlands Graduate School obejmują wszystkie te tematy z wyjątkiem ostatniego (monady). Obecnie dostępnych jest wiele innych zasobów dla monad. To nie jest duża strata.

Im więcej matematyki znasz, tym łatwiej będzie nauczyć się teorii kategorii. Ponieważ teoria kategorii jest ogólną teorią struktur matematycznych, pomocne jest poznanie niektórych przykładów, aby docenić znaczenie definicji. (Kiedy nauczyłem się teorii kategorii, musiałem tworzyć własne przykłady, wykorzystując swoją wiedzę na temat semantyki języka programowania, ponieważ standardowe podręczniki zawierały tylko przykłady matematyczne, o których nic nie wiedziałem.) Potem pojawiła się genialna książka Lambka i Scott nazwał „ Wprowadzenie do logiki kategorycznej„którą powiązaną teorię kategorii z systemami typów (co nazywają„ logiką ”). Można teraz zrozumieć teorię kategorii po prostu przez powiązanie jej z systemami typów nawet bez znajomości wielu przykładów. Wiele zasobów, o których wspomniałem powyżej, korzysta z tego podejście do wyjaśnienia teorii kategorii.

Postaram się, aby było to krótkie i słodkie. Istnieje nieformalna korespondencja między programami Haskell a niektórymi klasami kategorii, która może być bardziej formalna przy pewnej pracy. Ta korespondencja jest znana jako korespondencja Curry-Howard-Lambek i dotyczy:

1. Typy Haskella z obiektami kategorii
2. $A\rightarrow B$ $f\colon A\rightarrow B$
3. Algebraiczne typy danych z obiektami początkowymi
4. Pisz konstruktory z funktorami
5. itp

Lista jest długa, ale jednym z kluczowych punktów jest to, że możesz definiować takie rzeczy jak monady i algebry w teorii kategorii i wymyślać pojęcia, które są przydatne zarówno matematykom, jak i są wszechobecne w praktyce programowania Haskell.

Nie jestem pewien, którą książkę polecić, ponieważ nie znalazłem całkowicie zadowalającej książki wprowadzającej na temat kategorii dla informatyków. Możesz wypróbować kategorie, typy i struktury autorstwa Asperti i Longo. Chodzi o to, aby nauczyć się podstawowych definicji aż do adiunkcji, a następnie może spróbować przeczytać kilka doskonałych blogów, aby spróbować zrozumieć te pojęcia.

Nawiązując do porady @AJed, zalecam odwrócenie swojego oświadczenia

I want to learn category theory so I can become better at Haskell.

na głowie: naucz się Haskell, bazując na intuicji programistycznej. Gdy jesteś guru FP, łatwiej jest podnieść teorię kategorii (jeśli nadal ci zależy).

Teoria kategorii jest prosta dla osób z szerokim wykształceniem matematycznym (grupy, pierścienie, moduły, przestrzenie wektorowe, topologia itp.). Bez tego tła teoria kategorii jest prawie nieprzenikniona. Piękno teorii kategorii polega na tym, że jednoczy ona wiele pozornie niezwiązanych ze sobą rzeczy (np. Lewe punkty zapominających funktorów obejmują wolne grupy, uniwersalne algebry otaczające, kompaktacje Stone-Cech, abelianizacje grup, ...), a zatem zmniejsza złożoność. Ale jeśli nie znasz wielu przykładów, które łączą teorię kategorii, teoria kategorii jest tylko dodatkową warstwą złożoności, która utrudnia twoje życie.

Z mojego doświadczenia wynika, że ​​uczenie się jest łatwiejsze dzięki wykorzystaniu wiedzy, którą już znasz. Jako programista dużo wiesz o programowaniu, a programowanie w Haskell nie różni się tak bardzo od innych programów, więc zalecam podejście do Haskella z pragmatycznego punktu widzenia programowania, ignorując teorię kategorii. Trochę teorii kategorii, która znajduje się w Haskell, np. Pewne wsparcie dla monad, jest znacznie łatwiejsze dla programisty, aby uchwycić go bez objazdu przez teorię kategorii. W końcu monady są jedynie uogólnioną kompozycją (i już używałeś monad w swojej praktyce programistycznej - choć nie wiedząc, że tak robiłeś), a Haskell tak naprawdę nie wspiera monad, ponieważ nie egzekwuje praw monadycznych.

Krótka odpowiedź: nie [ale to tylko opinia]

Nie idź do teorii kategorii ani żadnej innej dziedziny teoretycznej, aby stać się dobrym w Haskell. Naucz się funkcjonalnych technik programowania, takich jak rekurencja ogona, mapa, redukcja i inne. Przeczytaj jak najwięcej kodu. Wdrożyć jak najwięcej pomysłów. Jeśli masz problemy, czytaj i czytaj.

Jeśli chcesz mieć dobre odniesienie teoretyczne do nauki Haskella i innych paradygmatów programowania funkcjonalnego, spójrz na: Wprowadzenie do programowania funkcjonalnego za pomocą rachunku lambda, Greg Michaelson (dostępny online). ... Istnieją inne podobne książki.

Oto (długi) post na blogu, który motywuje, w jaki sposób pomysły teorii kategorii są istotne dla praktycznego programowania: http://cdsmith.wordpress.com/2012/04/18/why-do-monads-matter/

Teoria kategorii jest bardzo wyrafinowaną gałęzią matematyki, a jej opanowanie zjednoczy większość twoich wcześniejszych nauk, czyniąc z nich instancje tych samych abstrakcyjnych obiektów. Jest to więc bardzo przydatne i bardzo intuicyjne. Ale jest rozległa i szeroka, a znajdziesz wiele nowych koncepcji, które nawet nie będą wiedziały, która jest odpowiednia dla twoich potrzeb, a którą należy pominąć. Więc twoje celowe podejście wymaga wyboru między pojęciami, w przeciwnym razie opanowanie go nieuchronnie wymaga długiego czasu i tak naprawdę nie jest domeną samokształcenia.

Nawiasem mówiąc, proponuję bardzo dobry punkt wyjścia, aby twój cel był tutaj .