Teoria kategorii (nie) dla programowania?

Po nauce języka Haskell i innych niezbyt czystych języków FP postanowiłem przeczytać o teorii kategorii. Po dobrym zrozumieniu teorii kategorii zacząłem myśleć o tym, jak pojęcia teorii kategorii można wykorzystać do projektowania programów, ale bez względu na to, jak bardzo się starałem, nie jest to dobra droga.

Po wielu nieudanych próbach powiązania teorii kategorii z projektowaniem programów doszedłem do wniosku, że:

Teoria kategorii jest przydatna przy projektowaniu języka programowania .
Teoria kategorii nie jest czymś, czego używasz podczas projektowania programów (nawet jeśli używasz języka, który został zaprojektowany w oparciu o zasady kategorii). Na przykład: Podczas programowania w Haskell będziesz używać typów, konstruktorów typów, funkcji, funkcji wyższego rzędu itp. Do projektowania programu, a nie pojęć teorii kategorii.

Podsumowując, mamy system warstwowy (kolejność od niskiej do wysokiej):

Teoria kategorii -> Język programowania -> Program

Na konkretnej warstwie korzystasz z koncepcji bezpośredniej warstwy podstawowej .

Czy to zrozumienie jest prawidłowe? Jeśli nie, a uważasz, że przy projektowaniu programów możemy bezpośrednio korzystać z koncepcji teorii kategorii, zapoznaj się z niektórymi artykułami lub postami na blogu, gdzie są one demonstrowane.

UWAGA: Projektując programy, mam na myśli projektowanie programów opartych na różnych koncepcjach, takich jak współbieżność, równoległość, reaktywność, przekazywanie wiadomości itp.

functional-programming category-theory

— Ankur
źródło

Czy uważasz monady za część języka programowania lub programów? Strzały?

— Dave Clarke

To wydaje mi się przynajmniej częściowo pytaniem filozoficznym. Nie jestem pewien, czy istnieje jedna poprawna odpowiedź. Jeden adept teorii kategorii zastosuje intuicję uzyskaną podczas programowania, inny będzie faworyzował różne sposoby myślenia.

— Raphael

Większość pisanych programów używa języków programowania, których nie inspiruje teoria kategorii. O ile mogę stwierdzić, przeciętny programista nie jest świadomy teorii kategorii, więc większość programów (w tym system operacyjny i przeglądarka) nie jest inspirowana wyższą matematyką.

— Yuval Filmus

@YuvalFilmus: Moje pytanie dotyczy funkcjonalnych języków programowania

— Ankur,

zobacz także to pytanie dla niektórych zastosowań monoidów w CS

— vzn

Odpowiedzi:

Cóż, to oczywiście zależy od tego, jaki program próbujesz zaprojektować.

Jeśli projektujesz program księgowy dla sklepu z czekoladą twojej ciotki, bardzo wątpię, czy teoria kategorii będzie bardzo przydatna.

Ale są oczywiście sytuacje, w których teoria kategorii jest niezwykle przydatna w projektowaniu programów (przez które rozumiem również struktury danych, biblioteki itp.). Takie sytuacje występują najczęściej, gdy zaangażowane programy mają charakter matematyczny.

Jeśli chcesz pisać programy, które obliczają dokładne liczby rzeczywiste i inne struktury występujące w analizie matematycznej, pierwszym pytaniem, na które musisz odpowiedzieć, jest to, co oznacza poprawne wdrożenie skomplikowanego obiektu matematycznego (takiego jak funkcja różniczkowalna, rozmaitość itp. ). Tutaj bardzo pomaga znajomość teorii i logiki kategorii, ponieważ zapewniają one systematyczny sposób tłumaczenia definicji struktur matematycznych na specyfikacje i implementacje odpowiednich struktur danych. Modne hasło, którego powinieneś szukać, to teoria wykonalności . Ale to tylko jeden przykład.

Najlepszym sposobem na sprawdzenie, w jaki sposób teoria kategorii się przydaje, jest przyjrzenie się programom napisanym przez ludzi znających wiele teorii kategorii (i ogólnie matematyki). Oczywistym tego przykładem jest Martín Escardó i jego niemożliwe funkcje, na przykład:

M. Escardó i P. Oliva: What Sequential Games, Tychonoff Theorem and Double-Negation Shift mają wspólne , matematyczne strukturyzowane programowanie funkcjonalne 2010, ACM Press. (z towarzyszącymi plikami Haskell i Agda )

Możesz narzekać, że to nie tylko teoria kategorii, ale także logika i topologia. Takie skargi byłyby bardzo mylne. Najlepsza teoria kategorii jest zawsze mieszana z innymi rzeczami.

Na koniec odradzałbym wyciąganie wielkich wniosków na temat natury rzeczy na podstawie odrobiny samodzielnego czytania.

— Andrej Bauer
źródło

Właśnie o to mi chodzi. Jeśli projektuję oprogramowanie księgowe, to moim typem projektowania będzie system typów. Jeśli nawet projektuję oprogramowanie matematyczne, użyję systemu typów do przedstawienia koncepcji teorii kategorii. Co w zasadzie wskazuje, że teoria typów Układy typu OR są bardziej ogólnymi abstrakcjami niż teorią kategorii.

— Ankur,

To śmieszne oświadczenie. Myślę, że powinieneś nauczyć się czegoś więcej, zanim wypowiesz takie ogólne oświadczenia. Być może możesz zacząć od egzystencji.wordpress.com/2011/03/27/the-holy-trinity

— Andrej Bauer

Nie jestem naukowcem, doktorem, naukowcem, matematykiem ani teoretykiem kategorii, więc nie denerwujcie się moimi wypowiedziami, nie będą one publikowane w żadnym czasopiśmie naukowym ani w pracach badawczych. Jestem tylko programistą, który próbuje zrozumieć drugą stronę medalu. Nawiasem mówiąc, dzięki za link.

— Ankur

Zdaję sobie z tego sprawę i właśnie dlatego sugeruję, abyś ostrożnie wyciągał wnioski tak jak ty: po prostu nie masz informacji wymaganych do wyciągnięcia takich wniosków. I właśnie dlatego odsyłam cię do postu na blogu Boba Harphera, a nie, powiedzmy, jakiejś technicznej książki na temat związku między teorią typów a teorią kategorii. Próbuję ci pomóc, ale w zamian oczekiwałbym od ciebie nieco większej rezerwy, jeśli chodzi o wyciąganie wielkich wniosków na temat natury całej gałęzi matematyki.

— Andrej Bauer,

Na przykład stwierdziłeś, że „teoria typów jest bardziej ogólną abstrakcją niż teorią kategorii”. To jest przykład stwierdzenia, którego powinieneś nie opierać na małej wiedzy. Pracuję profesjonalnie w tej dziedzinie i nawet ja byłbym bardzo ostrożny, aby wyciągnąć taki lub przeciwny wniosek.

— Andrej Bauer,

Ludzie używali CT do opisywania typów danych.

Typ danych został zdefiniowany przez określoną kategorię, której obiekty są skończonymi sekwencjami typów (język specyfikacji) i których strzałki były rzutami lub kompozycjami operacji typu danych. Na przykład obiekt jest domeną i jest kodomainą operacji wypychania stosów. To daje ci składnię, ale nadal nie masz pojęcia semantyki.
Algebra, czyli instancja tego typu, jest funktorem od teorii do Ens, kategorii (małych) zbiorów. (Używamy „małych”, aby uniknąć paradoksu Russella, ale to nie ma większego znaczenia.)
Okazuje się, że właściwości zamknięcia kategorii odpowiadają rodzinom teorii logicznych. Na przykład, jeśli kategoria teorii jest zamknięta pod produktami, typ danych można aksjatyzować za pomocą równań. Jeśli kategoria teorii zostanie zamknięta przez wycofanie, wówczas typ danych można aksjatyzować za pomocą zdań Horn.

Nie jestem do końca pewien, czy ktokolwiek zwraca na to uwagę. Sądzę, że to i zawarte tam linki wyjaśniłyby to bardziej szczegółowo.

— Vilcxjo
źródło