Żądanie referencyjne: Teoria kategorii w odniesieniu do układów typów

Ciągle słyszę o tym, jak należy nauczyć się teorii kategorii, aby naprawdę zrozumieć teorię języka programowania. Do tej pory nauczyłem się sporo PL bez wchodzenia w sferę kategorii. Uznałem jednak, że nadszedł czas, aby zrobić krok, aby zobaczyć, co straciłem.

Niestety, żadne ze źródeł, które mogę znaleźć, nie wydają się tworzyć żadnych połączeń z systemami typu lub programowaniem. Mówią , że jest to wprowadzenie do teorii kategorii dla informatyków, ale potem przechodzą w ogólne abstrakcyjne bzdury (mówię to z miłością) bez podawania praktycznych przykładów lub zastosowań.

Wydaje mi się, że moje pytanie jest dwojakie:

Czy teoria kategorii jest niezbędna do zrozumienia „głębokich pojęć” w PL?
Jakie źródło wyjaśnia teorię kategorii z punktu widzenia praktycznych zastosowań systemów typu i programowania?

Jak dotąd najdalej posunąłem się do niejasnej koncepcji funktorów (które, jak mi się wydaje, nie są powiązane z funktorami w ML). Boję się abstrakcji, którą muszę zachować w głowie, aby zrozumieć monady z teoretycznego punktu widzenia.

— ogrodnik
źródło

@Raphael Zadawanie pytań składających się z dwóch różnych pytań jest tylko słabo ze sobą powiązane. Ale pytanie 1. nie jest subiektywne. Jest to raczej prośba o wyjaśnienia i wyjaśnienia. Wydaje mi się, że pytanie 2. miało na myśli to, że jest zadowolony z odniesienia do miejsca, w którym jest wyjaśnione, a nie z faktycznego wyjaśnienia.

— Thomas Klimpel

W przyszłości lepiej zadać tylko jedno pytanie na post. Możesz zadać pytanie 1, a następnie w zależności od otrzymanych odpowiedzi zdecydować, czy zadać pytanie 2 osobno. To często sprawia, że wszystko idzie płynniej.

— DW

@Raphael Jak pytanie jest subiektywne? Trudno jest ocenić - czy o to ci chodzi? I może mieć odpowiedź: „To zależy od tego, jaką osobą jesteś”. - czy o to Ci chodziło? Nadal może się okazać, że jest to absolutnie niezbędne, czy zdecydowanie nie konieczne, prawda? (I ludzie wydają się zgadzać, że nie jest to konieczne.)

— k.stm

@ k.stm Martwi mnie ogólny kształt pytania. Gdyby ktoś zapytał: „Czy algebra jest niezbędna do zrozumienia głębokich pojęć języków formalnych?”, Wiem na pewno, że różni ludzie udzielają różnych odpowiedzi - w zależności od ich preferencji i gustu. Nie oczekuję, że będzie inaczej.

— Raphael

@Raphael Dobra, rozumiem. Ale myślę, że to ludzie udzielający subiektywnych odpowiedzi na obiektywne pytanie. (Czuje się, jakby ludzie mówili „Och, piję pięć filiżanek dziennie i czuję się świetnie!”, Kiedy pytają, czy kawa jest zdrowa, czy nie.)

— k.stm

Odpowiedzi:

Teoria kategorii nie jest konieczna do zrozumienia języków programowania, nie jest nawet konieczne prowadzenie zaawansowanych badań nad językami programowania. Większość osób posługujących się językiem programowania nie zna teorii kategorii.

Metody teoretyczne kategorii były przydatne głównie w niewielkiej części badań nad językiem programowania, a mianowicie w analizie programowania funkcjonalnego, szczególnie od czasu wielkiego odkrycia Moggi'ego, że niektóre efekty obliczeniowe mają strukturę monadyczną. W latach 90., po przełomie Moggi'ego, przeprowadzono wiele badań, aby rozszerzyć metody kategoryczne na inne formy języków programowania. Jednak, zgodnie z moją najlepszą wiedzą, metody kategoryczne nie zostały uznane za przydatne w przypadku OO, obliczeń współbieżnych, równoległych i rozproszonych, obliczeń czasowych lub kompilatorów. Z tego powodu ludzie w większości porzucili rozszerzanie metod kategorycznych.

Podejścia kategoryczne do programowania maszynowego sprawdzają się w czystych funkcjach. Rzeczywiście niektóre proste systemy pisania są kategoriami. Jest to opisane np

Kategorie dla typów według Roy Crole
Wprowadzenie do kategorycznej logiki wyższego rzędu przez Joachima Lambka i Phila Scotta.

Obecnie jest wiele pracy nad typami dla współbieżnych procesów (np. Typy sesji) i żaden z nich nie ma charakteru kategorycznego od września 2016 r.

To powiedziawszy, nigdy nie można wiedzieć zbyt dużo matematyki, a znajomość teorii kategorii jest przydatna. Jest to więc kwestia kosztów / korzyści. Jeśli lubisz matematykę, jeśli masz trochę doświadczenia w algebrze (np. Jaka jest wolna grupa w zbiorze, wolny pierścień itp.), Teoria kategorii uczenia się będzie łatwa, a jeśli planujesz wykonywać pracę, która jest (inspirowana) programowanie funkcjonalne, przydatne będą znajomości kategorii.

Wreszcie teoria kategorii jest piękną matematyką i warto ją studiować tylko dlatego, że jest taka schludna.

Zobacz udział Uday Reddy w tej dyskusji, aby zobaczyć inne zdanie.

— Martin Berger
źródło

„Jednak, zgodnie z moją najlepszą wiedzą, metody kategoryczne nie okazały się tak przydatne dla…” To jest właśnie mój problem. Semantyka operacyjna może dokładnie opisać wszystkie te pojęcia, więc nie czułem się tak, jakby mi tego brakowało. Kocham matematykę, ale niestety brakuje mi doświadczenia w algebrze abstrakcyjnej. Rozumiem jedynie podstawowe zasady typowych struktur algebraicznych. Sprawiło to, że chwytanie teorii kategorii jest szczególnie kłopotliwe.

— ogrodnik

@gardenhead W takim razie może CT nie jest dla ciebie tak przydatne. Jeśli chcesz przeczytać dużo artykułów w przestrzeni „Programowanie funkcjonalne”, w tym pracę na typach, to wiele z nich będzie używać języka CT.

— Martin Berger,

Czy to jest duplikat?

— Raphael

Chciałbym dodatkowo zasugerować książkę cs.unibo.it/~asperti/PAPERS/book.pdf „Kategorie, typy i struktury”, która jest najwyraźniej wyczerpana, ale jest to link do pliku pdf z jednego z strony domowe autorów, więc sądzę, że jest to uzasadnione.

— John Forkosh

Teoria kategorii uczenia się to ogromna inwestycja czasowa, a pytanie, czy warto, jest bardzo ważne. Nadal mam z tym problem i już wiem, dlaczego powinienem się tego nauczyć. Napisałem:

Kiedy zaczynałem programować, lubiłem język asemblera, a teoria zbiorów jest podobna do języka asemblera. Teoria kategorii jest jedną z alternatyw dla obejścia wszystkich zakorzenionych uprzedzeń dotyczących logiki i teorii modeli osadzonych w głównym nurcie teorii zbiorów ZFC.

Chodzi tutaj o użycie kategorii zamiast zbiorów lub „nieokreślonych bitów” jako możliwej semantyki dla teorii typów lub języka programowania. Dlaczego warto to robić? Rozważ dualność między działaniem a obserwacją. Różne obserwacje (lub przynajmniej ich kolejność w czasie) nie kolidują ze sobą (poza mechaniką kwantową), ale niekoniecznie dotyczy to różnych działań. Ugruntowane uprzedzenia dotyczące logiki osadzone w teorii zbiorów utrudniają modelowanie działań w porównaniu z obserwacjami modelowania.

Nie jestem przekonany, że tak naprawdę istnieje idealna zgodność między teorią kategorii a teorią typów, jak stwierdzono tutaj :

Przez dualność składniowo-semantykę można postrzegać teorię typów jako formalny język lub rachunek syntaktyczny dla teorii kategorii, i odwrotnie, można myśleć o teorii kategorii jako zapewniającej semantykę dla teorii typów.

To prawda, że teoria kategorii może zapewnić semantykę dla teorii typów (co może być naprawdę przydatne), ale wątpię, czy teoria typów naprawdę zapewnia wystarczająco potężny formalny język syntaktyczny do wyrażenia wszystkich obliczeń wykonanych w teorii kategorii.

W praktyce przydatność teorii kategorii może wynikać z sugestii przydatnych pytań i analogii. Ale teoria kategorii może również sugerować działania i pytania, które ostatecznie okazują się po prostu odwracaniem uwagi (stratą czasu) od naprawdę ważnych kwestii. Z pewnością możesz nauczyć się logiki i teorii typów bez dbania o teorię kategorii.

— Thomas Klimpel
źródło

Dziękuję za twoje przemyślenia. Twoje powody, dla których teoria kategorii uczenia się wydają się inne niż moje; Twoje zainteresowania wynikają z czysto matematycznej perspektywy, a ja chciałbym poszerzyć moje rozumienie typów. Mimo to miło jest wiedzieć, że innym osobom poza mną trudno znaleźć kategorię, do której można się zgłosić i zgłosić

— ogrodnik