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
fa: A → BZABf
ABf
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 .
×→Listwł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.