Jaki jest związek między funktorami w SML i teorii kategorii?

W tym samym myśleniu, co wypowiedź Andreja Bauera w tej odpowiedzi

Społeczność Haskell opracowała szereg technik inspirowanych teorią kategorii, z których najlepiej znane są monady, ale nie należy ich mylić z monadami .

Jaki jest związek między funktorami w SML a funktorami w teorii kategorii?

Ponieważ nie znam szczegółów funktorów w innych językach, takich jak Haskell lub OCaml, jeśli są informacje o wartości, proszę również dodać sekcje dla innych języków.

Kategorie tworzą (dużą) kategorię, której obiektami są (małe) kategorie, a morfizmy są funktorami między małymi kategoriami. W tym sensie funktory w teorii kategorii są „morfizmami większych rozmiarów”.

Funktory ML nie są funktorami w kategorycznym znaczeniu tego słowa. Są to jednak „funkcje o większym rozmiarze” w sensie teoretycznym.

Pomyśl o konkretnych typach danych w typowym języku programowania jako o „małych”. Tak więc int, bool, int -> intitp są małe, zajęcia w języku Java są małe, jak również w elemencie C. Możemy zebrać wszystkie typy danych do dużej kolekcji o nazwie Type. Konstruktor typów, taki jak listlub arrayjest funkcją od Typedo Type. Jest to więc „duża” funkcja. Funktor ML jest tylko nieco bardziej skomplikowaną dużą funkcją: przyjmuje jako argument kilka małych rzeczy i zwraca kilka małych rzeczy. „Kilka małych rzeczy razem” jest znane jako struktura w ML. Pod względem teorii typów Martina-Löfa mamy wszechświat Type małych typów. Duże typy są zwykle nazywane rodzajami . Więc mamy:

1. wartości są elementami typów (przykład 42 : int:)
2. typy są elementami Type(przykład int : Type:)
3. Podpisy ML są rodzajami (przykład OrderedType:)
4. Konstruktory typów są elementami rodzajów (przykład list : Type -> Type:)
5. Konstrukcje ML są elementami typu (np String : OrderedType)
6. Funktory ml w funkcji między rodzaju (np Map.Make : Map.OrderedType -> Make.S)

Teraz możemy narysować analogię między ML a kategoriami, w których funktory odpowiadają funktorom. Ale zauważamy również, że typy danych w ML są jak „małe kategorie bez morfizmów”, innymi słowy, są bardziej jak zbiory niż kategorie. Możemy zastosować analogię między ML a teorią zbiorów:

1. typy danych są jak zestawy
2. rodzaje są jak klasy teoretyczne
3. funktory są jak funkcje wielkości klasy

Standardowa struktura ML jest podobna do algebry . Jego podpis opisuje całą klasę algeb o podobnym kształcie.

Standardowy funktor ML to mapa od klasy algeb do innej klasy algeb. Analogią jest na przykład funktory , która dodaje operację odwrotną do monoidów, lub która dodaje multipoidatywna monoida do grup abelowych, aby tworzyć pierścienie.$F : {\bf Mon} \to {\bf Grp}$$F : {\bf Ab} \to {\bf Rng}$

Większość tych pomysłów została opracowana w serii artykułów przez Burstall i Goguen przy projektowaniu języka specyfikacji o nazwie CLEAR (odniesienia c5 i c6 na stronie DBLP ). David MacQueen współpracował wówczas z Burstallem i Sannellą i był blisko z problemami. Standardowy system modułów ML opiera się na tych pomysłach.

Co większość ludzi by się zastanawiała, co z morfizmami? Teoretyczne funktory kategorii mają część przedmiotową i część morficzną. Czy standardowe funktory ML mają to samo? Odpowiedź brzmi TAK i NIE.

• Odpowiedź TAK ma zastosowanie, jeśli struktury są pierwszego rzędu. Następnie występują homomorfizmy między różnymi strukturami tego samego podpisu, a standardowe funktory ML automatycznie mapują je na homomorfizmy podpisu wynikowego.
• NIE, część odpowiedzi ma zastosowanie, gdy struktury mają operacje wyższego rzędu.

Czy to oznacza, że ​​Standard ML odbiega od teorii kategorii? Nie wydaje mi się Raczej myślę, że Standard ML robi dobrze, a teoria kategorii jeszcze nie nadrobiła zaległości. Teoria kategorii nie wie jeszcze, jak radzić sobie z funkcjami wyższego rzędu. Pewnego dnia to zrobi.

Według mojej najlepszej wiedzy nie ma formalnego związku między funktorami w teorii kategorii i funktorami w ML (SML lub OCaml, są one wystarczająco bliskie dla naszego celu tutaj).

W teorii kategorii funktory to funkcje, które działają na obiektach. Są o jeden poziom powyżej morfizmów, które często są funkcjami działającymi na elementy (wiele kategorii ma obiekty, które są zestawami o pewnej strukturze algebraicznej i strzałki, które są homomorfizmami między tymi strukturami). Funktor ML to funkcja działająca na modułach, jeden poziom powyżej funkcji działających na wartościach języka podstawowego. Myślę, że podobieństwo się tu kończy.

Funktory ML zostały ochrzczone przez Dave'a McQueena w jego wydanej w 1985 r. Wersji Modules for Standard ML (citeseerx), która ukazała się w Biuletynie Polimorficznym (oryginalny artykuł używał wyrażenia „moduł parametryczny” - późniejsze publikacje używają przymiotnika „sparametryzowany”). Niestety nie mogę znaleźć kopii tego papieru. W swoim artykule z 1986 r. Używanie typów zależnych do wyrażania struktury modułowej (citeseerx) podaje nazwę jako ustaloną.