Die Kategorietheorie findet Anwendung in der theoretischen Informatik und ist offensichtlich von zentraler Bedeutung für die abstrakte Mathematik. Ich habe gehört, dass es auch direkte praktische Anwendungen in der Programmierung und Softwareentwicklung hat.
Für welche Art der Programmierung ist die praktische Kategorietheorie notwendig? Was erreichen Programmierer mit der Kategorietheorie?
Bitte beachte meine Verwendung von "notwendig" und "erforderlich" in diesem Beitrag. Mir ist klar, dass die meisten Programmierer in gewissem Sinne von der Erfahrung mit verschiedenen Arten von Theorien profitieren werden, aber ich suche nach direkten Anwendungen, bei denen die Verwendung der Kategorietheorie wesentlich ist, dh wenn Sie die Kategorietheorie nicht kennen, können Sie dies wahrscheinlich nicht Tu es.
Außerdem möchte ich klarstellen, dass ich durch "welche Art von Programmierung" weniger auf eine umfassende Antwort wie "funktionale Programmierung" als vielmehr auf bestimmte Anwendungen wie "Schreiben von Banksoftware" oder "Erstellen von Betriebssystemen" hoffe.
quelle
Antworten:
Die Frage stellt sich nach einem abstrakten mathematischen Konzept (Kategorietheorie) und hofft auf eine sehr praktische Antwort (spezifische Anwendungen). Bei allem Respekt halte ich dies für eine unrealistische Erwartung.
Abstrakte mathematische Konzepte sind Teil der Grundlagen von Programmiersprachen, nicht von Anwendungen. Beispielsweise spielen Datentypen eine zentrale Rolle bei der Programmierung. Jede Sprache hat irgendeine Form von Datentypen und implementiert ein Typsystem - ob statisch oder dynamisch, stark oder schwach, explizit oder implizit usw. Es gibt jedoch keinen Standard.
Daher haben viele Informatiker versucht, mithilfe der Kategorietheorie ein einheitliches Typsystem zu definieren . Siehe zum Beispiel Haginos Categorical Programming Language (1987) und Charity (1996), dann ML (2003) und CAML und natürlich Haskell , die eine "Haskell-Kategorie" von Typen definieren, und Haskell-Funktionen sind Morphismen auf Typen ...
Dies ist der Fall, weil die Typentheorie eng mit der Kategorietheorie verwandt ist . Um JL Bell zu zitieren: "Kategorien können selbst als Typentheorien einer bestimmten Art angesehen werden ... Somit ist die Typentheorie viel enger mit der Kategorietheorie verbunden als mit der Mengenlehre ... Grob gesagt kann man sich eine Kategorie vorstellen als eine Typentheorie, die ihrer Syntax beraubt ist. " Es wurde gezeigt, dass zum Beispiel kartesische geschlossene Kategorien typisiertem λ-Kalkül entsprechen und C-Monoide untypisiertem λ-Kalkül entsprechen ...
Ich denke nicht, dass Kategorietheorie für irgendeine Art von Programmierung notwendig ist , aber es ist ein sehr nützliches Werkzeug beim Entwerfen und Implementieren von Programmiersprachen, und insbesondere. diejenigen, die von Natur aus mathematisch sind. Aus diesem Grund wird die funktionale Programmierung häufig als kategoriale Programmierung bezeichnet, und alle oben genannten Programmiersprachen sind FP-Sprachen.
Eine empfohlene Einführung in das Thema ist " Ein Vorgeschmack auf die Kategorietheorie für Informatiker " von BC Pierce (1988). Diese und andere nützliche Informationen wurden in einer ähnlichen Diskussion über Mathoverflow gefunden .
quelle
Es ist wie im Org-Modus für Banken.
Mir ist klar, dass das vage ist, aber Sie haben gesagt, Sie wollten eine praktische Antwort.
In Kategorien dreht sich alles um Dualität (oder zumindest sehe ich das so) aufgrund des Axioms der Wahl. Ich persönlich würde sagen, es wäre eine dumme Art, ein einheitliches Typsystem einzuführen, obwohl es sich um einen Typ selbst handelt (eine Instanz von a Typ) ist im Grunde eine Kategorie.
Einfach getippte Lambda-Kalküle haben kein axiomatisches Typensystem, weshalb sie als Grundlage für die Typentheorie gelten. Dies unterscheidet sich von Lambda-Kalkülen, die ein geeignetes Typsystem verwenden.
Einfach getippter Lambda-Kalkül normalisiert sich stark und obwohl das Abgleichen von Typen ziemlich langweilig ist, ist die Logik solide.
Auch unendlich / abhängig typisierter Lambda-Kalkül (oder rein typisierter) normalisiert sich nicht richtig, da er einen Typ für alle Typen hat, der im Grunde ein kirchenkodiertes Typensystem ist.
Kategorien sind überall, aber von Natur aus fast nicht sofort zu sehen.
quelle