Entsprechend dieser Aussage von Andrej Bauer in dieser Antwort
Die Haskell-Community hat eine Reihe von Techniken entwickelt, die von der Kategorietheorie inspiriert sind. Monaden sind am bekanntesten, sollten aber nicht mit Monaden verwechselt werden .
Welche Beziehung besteht zwischen Funktoren in SML und Funktoren in Kategorietheorie?
Da ich keine Informationen über Funktoren in anderen Sprachen wie Haskell oder OCaml habe, fügen Sie bitte auch Abschnitte für andere Sprachen hinzu, wenn Informationen von Wert vorhanden sind.
Antworten:
Kategorien bilden eine (große) Kategorie, deren Objekte die (kleinen) Kategorien sind und deren Morphismen Funktoren zwischen kleinen Kategorien sind. In diesem Sinne sind Funktoren in der Kategorietheorie "Morphismen höherer Größe".
ML-Funktoren sind keine Funktoren im eigentlichen Sinne des Wortes. Aber es sind "Funktionen höherer Größe" im typentheoretischen Sinne.
Stellen Sie sich konkrete Datentypen in einer typischen Programmiersprache als "klein" vor. So
int
sindbool
,int -> int
etc, klein, Klassen in Java sind klein, ebenso Strukturen in C. Wir können alle Datentypen in einer großen Sammlung namens sammelnType
. Ein Typkonstruktor wielist
oderarray
ist eine Funktion vonType
bisType
. Es ist also eine "große" Funktion. Ein ML-Funktor ist nur eine etwas kompliziertere große Funktion: Er akzeptiert als Argument mehrere kleine Dinge und gibt mehrere kleine Dinge zurück. "Mehrere kleine Dinge zusammenfügen" ist in ML als Struktur bekannt . Im Sinne der Martin-Löf-Typentheorie haben wir ein UniversumType
kleiner Typen. Die großen Arten werden gewöhnlich Arten genannt . Also haben wir:42 : int
)Type
(Beispielint : Type
)OrderedType
)list : Type -> Type
)String : OrderedType
)Map.Make : Map.OrderedType -> Make.S
)Jetzt können wir eine Analogie zwischen ML und Kategorien ziehen, unter denen Funktoren Funktoren entsprechen. Wir bemerken aber auch, dass Datentypen in ML wie "kleine Kategorien ohne Morphismen" sind, mit anderen Worten, sie sind eher wie Mengen als wie Kategorien. Wir könnten dann eine Analogie zwischen ML und Mengenlehre verwenden:
quelle
Eine Standard-ML-Struktur ähnelt einer Algebra . Seine Signatur beschreibt eine ganze Klasse von Algebren ähnlicher Form.
Die meisten dieser Ideen wurden in einer Reihe von Artikeln von Burstall und Goguen ausgearbeitet, in denen eine Spezifikationssprache namens CLEAR entworfen wurde (Referenzen c5 und c6 auf der DBLP-Seite ). David MacQueen arbeitete zu dieser Zeit eng mit Burstall und Sannella zusammen und war vertraut mit den Fragen. Das Standard ML-Modulsystem basiert auf diesen Ideen.
Was sich die meisten Leute fragen würden, ist, was ist mit Morphismen? Kategorietheoretische Funktoren haben einen Objektteil und einen Morphismusteil. Haben Standard ML Funktoren die gleichen? Die Antwort lautet JA und NEIN.
Bedeutet dies, dass Standard ML von der Kategorietheorie abweicht? Ich glaube nicht. Ich denke eher, dass Standard ML das Richtige tut und die Kategorietheorie noch nicht aufgeholt ist. Die Kategorietheorie kann noch nicht mit Funktionen höherer Ordnung umgehen. Eines Tages wird es.
quelle
Es gibt meines Wissens keine formale Beziehung zwischen Funktoren in der Kategorietheorie und Funktoren in ML (SML oder OCaml, sie sind nah genug für unseren Zweck hier).
In der Kategorietheorie sind Funktoren Funktionen, die Objekte bearbeiten. Sie befinden sich eine Ebene über Morphismen, bei denen es sich häufig um Funktionen handelt, die auf Elemente angewendet werden (viele Kategorien haben Objekte mit einer bestimmten algebraischen Struktur und Pfeile, die Homomorphismen zwischen diesen Strukturen sind). Ein ML-Funktor ist eine Funktion, die für Module ausgeführt wird, eine Ebene über den Funktionen, die für Kernsprachenwerte ausgeführt werden. Ich denke, die Ähnlichkeit hört hier auf.
Die ML-Funktoren wurden 1985 von Dave McQueen in seiner Überarbeitung von Modules for Standard ML (citeseerx) getauft , die im Polymorphism Newsletter erschien . Leider kann ich keine Kopie dieses Papiers finden. In seiner Arbeit von 1986 über die Verwendung abhängiger Typen, um die modulare Struktur auszudrücken (citeseerx) nennt er den Namen als etabliert.
quelle