Ist Kategorietheorie nützlich, um funktionale Programmierung zu lernen?

Ich lerne Haskell und bin fasziniert von der Sprache. Allerdings habe ich keinen ernsthaften Mathe- oder CS-Hintergrund. Aber ich bin ein erfahrener Softwareprogrammierer.

Ich möchte Kategorietheorie lernen, damit ich bei Haskell besser werden kann.

Welche kategorietheoretischen Themen sollte ich lernen, um eine gute Grundlage für das Verständnis von Haskell zu schaffen?

In einer früheren Antwort auf der Website Theoretical Computer Science (Theoretische Informatik) habe ich gesagt, dass die Kategorietheorie die "Grundlage" für die Typentheorie ist. Hier möchte ich etwas Stärkeres sagen. Kategorietheorie ist Typentheorie . Umgekehrt ist Typentheorie Kategorietheorie . Lassen Sie mich auf diese Punkte eingehen.

Kategorietheorie ist Typentheorie

$f : A \to B$$A$$B$$f$

$A$$B$$f$

Die Typentheorie ist die Kategorietheorie

Mit "Typentheorie" meine ich jede Art von typisierter formaler Sprache, die auf starren Regeln der Termbildung basiert, die sicherstellen, dass alle Typen überprüft werden. Es stellt sich heraus, dass wir, wenn wir in einer solchen Sprache arbeiten, in einer kategorietheoretischen Struktur arbeiten. Selbst wenn wir Mengen-theoretische Notationen verwenden und Mengen-theoretisch denken, schreiben wir doch Dinge, die kategorisch Sinn machen. Das ist eine erstaunliche Tatsache .

In der Vergangenheit war Dana Scott möglicherweise die erste, die dies erkannte. Er arbeitete an der Erstellung semantischer Modelle von Programmiersprachen, die auf typisierter (und nicht typisierter) Lambda-Rechnung basierten. Die traditionellen satztheoretischen Modelle waren für diesen Zweck unzureichend, da Programmiersprachen eine uneingeschränkte Rekursion beinhalten, die theoretische Mängel beseitigt. Scott erfand eine Reihe semantischer Modelle, die Programmierphänomene erfassten, und stellte fest, dass die typisierte Lambda-Rechnung genau eine Klasse von Kategorien darstellte, die als kartesische geschlossene Kategorien bezeichnet wurde . Es gibt viele geschlossene kartesische Kategorien, die nicht "satztheoretisch" sind. Die typisierte Lambda-Rechnung gilt jedoch für alle gleichermaßen. Scott schrieb einen schönen Aufsatz mit dem Titel " Relating Theories of Lambda Calculus""Erklären, was los ist, von denen Teile im Internet verfügbar zu sein scheinen. Der ursprüngliche Artikel wurde in einem Band mit dem Titel" To HB Curry: Essays on Combinatory Logic, Lambda Calculus und Formalism ", Academic Press, 1980, veröffentlicht. Berry and Curien gelangte wahrscheinlich unabhängig zu derselben Erkenntnis: Sie definierten eine Categorical Abstract Machine (CAM), um diese Ideen bei der Implementierung von funktionalen Sprachen zu verwenden, und die Sprache, die sie implementierten, hieß "CAML", das zugrunde liegende Framework von Microsofts F # .

$\times$$\to$$List$genau, um das Konzept der polymorphen Funktionen zu formalisieren. Sie nannten sie "natürliche Transformationen", "natürlich", weil sie die einzigen sind, die Sie mit Typvariablen typrichtig schreiben können. Man könnte also sagen, dass die Kategorietheorie genau erfunden wurde, um polymorphe Programmiersprachen zu formalisieren, noch bevor Programmiersprachen entstanden sind!

Ein mengentheoretischer Traditionalist kennt die Funktionen und natürlichen Transformationen, die unter der Oberfläche ablaufen, wenn er mengentheoretische Notationen verwendet, nicht. Aber solange er das Typensystem treu benutzt, macht er wirklich kategoriale Konstruktionen, ohne sich dessen bewusst zu sein.

Die Kategorietheorie ist die fundamentale mathematische Theorie von Typen und Funktionen. Somit können alle Programmierer, insbesondere funktionale Programmierer, von etwas Kategorietheorie profitieren. Leider scheint es keine Lehrbücher zur Kategorietheorie zu geben, die sich speziell an Programmierer richten. Die Bücher "Kategorietheorie für Informatik" richten sich in der Regel an theoretische Informatikstudenten / -forscher. Das Buch von Benjamin Pierce, Grundlagen der Kategorietheorie für Informatiker, ist vielleicht das am besten lesbare.

Es gibt jedoch viele Ressourcen im Web, die sich an Programmierer richten. Die Haskellwiki-Seite kann ein guter Ausgangspunkt sein. An der Midlands Graduate School halten wir (unter anderem) Vorlesungen über Kategorietheorie. Graham Huttons Kurs war als "Anfängerkurs" und meiner als "Fortgeschrittenenkurs" festgelegt. Beide behandeln jedoch im Wesentlichen den gleichen Inhalt und gehen in unterschiedliche Tiefen. Die University of Chalmers hat eine schöne Ressourcenseite mit Büchern und Vorlesungsskripten aus der ganzen Welt. Die begeisterte Blog-Seite von "sigfpe" bietet auch aus Sicht eines Programmierers eine Menge guter Intuitionen.

Die grundlegenden Themen, die Sie lernen möchten, sind:

• Definition von Kategorien und einige Beispiele für Kategorien
• Funktoren und Beispiele von ihnen
• natürliche Transformationen und Beispiele dafür
• Definitionen von Produkten, Nebenprodukten und Exponenten (Funktionsräumen), Anfangs- und Endobjekten.
• Zusätze
• Monaden, Algebren und Kleisli Kategorien

Meine eigenen Vorlesungsunterlagen in der Midlands Graduate School behandeln alle diese Themen mit Ausnahme der letzten (Monaden). Es gibt heutzutage viele andere Ressourcen für Monaden. Das ist also kein großer Verlust.

Je mehr Mathematik Sie kennen, desto einfacher ist es, Kategorietheorie zu lernen. Da es sich bei der Kategorietheorie um eine allgemeine Theorie mathematischer Strukturen handelt, ist es hilfreich, einige Beispiele zu kennen, um zu verstehen, was die Definitionen bedeuten. (Als ich Kategorietheorie lernte, musste ich meine eigenen Beispiele mit meinen Kenntnissen der Programmiersprachensemantik erfinden, da die Standardlehrbücher nur mathematische Beispiele enthielten, von denen ich nichts wusste.) Dann kam das brillante Buch von Lambek und Scott nannte " Einführung in die kategoriale Logik"Welche Kategorietheorie zu Typensystemen in Beziehung gesetzt wurde (was sie" Logik "nennen). Es ist jetzt möglich, Kategorietheorie zu verstehen, indem man sie nur zu Typensystemen in Beziehung setzt, auch ohne viele Beispiele zu kennen. Viele der oben erwähnten Ressourcen verwenden dies Ansatz zur Erklärung der Kategorietheorie.

Ich werde versuchen, es kurz und bündig zu halten. Es gibt eine informelle Korrespondenz zwischen Haskell-Programmen und bestimmten Klassen von Kategorien, die mit einigen Arbeiten formalisiert werden kann. Diese Korrespondenz ist als Curry-Howard-Lambek-Korrespondenz bekannt und bezieht sich auf:

1. Haskell- Typen mit Objekten der Kategorie
2. $A\rightarrow B$ $f\colon A\rightarrow B$
3. Algebraische Datentypen mit Anfangsobjekten
4. Geben Sie Konstruktoren mit Funktoren ein
5. usw

Die Liste geht weiter und weiter, aber ein entscheidender Punkt ist, dass Sie Dinge wie Monaden und Algebren in der Kategorietheorie definieren und sich Begriffe einfallen lassen, die sowohl für Mathematiker nützlich als auch in der Praxis der Haskell-Programmierung allgegenwärtig sind.

Ich bin mir nicht sicher, welches Buch ich empfehlen soll, da ich kein vollständig zufriedenstellendes Einführungsbuch zu Kategorien für Informatiker gefunden habe. Sie können Kategorien, Typen und Strukturen von Asperti und Longo ausprobieren. Die Idee ist, grundlegende Definitionen bis hin zu Zusätzen zu lernen und dann vielleicht einige der hervorragenden Blogs zu lesen , um zu versuchen, diese Konzepte zu verstehen.

Nach dem @AJed-Ratschlag empfehle ich, Ihre Aussage zu ändern

I want to learn category theory so I can become better at Haskell.

Auf den Kopf gestellt: Lernen Sie Haskell und bauen Sie dabei auf Ihre Programmierkenntnisse. Sobald Sie ein FP-Guru sind, ist es möglicherweise einfacher, die Kategorietheorie zu erlernen (wenn Sie sich immer noch darum kümmern).

Die Kategorietheorie ist für jemanden mit breiter mathematischer Ausbildung (Gruppen, Ringe, Module, Vektorräume, Topologie usw.) einfach. Ohne diesen Hintergrund ist die Kategorietheorie nahezu undurchdringlich. Das Schöne an der Kategorietheorie ist, dass sie viele scheinbar nicht miteinander verbundene Dinge vereint (z. B. linke Nachbarn von vergesslichen Funktoren sind freie Gruppen, universelle Hüllalgebren, Stone-Cech-Kompaktifizierungen, Abelianisierungen von Gruppen usw.) und so die Komplexität verringert. Aber wenn Sie nicht mit den vielen Beispielen vertraut sind, die die Kategorietheorie vereint, ist die Kategorietheorie nur eine zusätzliche Komplexitätsebene, die Ihr Leben schwieriger macht.

Nach meiner Erfahrung ist das Lernen einfacher, wenn man auf bereits bekannten Dingen aufbaut. Als Softwareentwickler wissen Sie viel über Programmierung, und die Haskell-Programmierung unterscheidet sich nicht wesentlich von anderen Programmen. Daher empfehle ich, Haskell aus pragmatischer Sicht der Programmierung zu nähern und dabei die Kategorietheorie zu ignorieren. Der Teil der Kategorietheorie, der in Haskell enthalten ist, z. B. die Unterstützung von Monaden, ist für einen Programmierer viel einfacher zu verstehen, ohne einen Umweg über die Kategorietheorie zu machen. Schließlich handelt es sich bei Monaden nur um verallgemeinerte Kompositionen (und Sie werden bereits Monaden in Ihrer Programmierpraxis verwendet haben - wenn auch ohne es zu wissen), und Haskell unterstützt Monaden nicht wirklich, da sie die monadischen Gesetze nicht durchsetzen.

Eine kurze Antwort: nein [aber dies ist nur eine Meinung]

Gehen Sie nicht in die Kategorietheorie oder einen anderen theoretischen Bereich, um in Haskell gut zu werden. Erlernen Sie funktionale Programmiertechniken wie die Schwanzrekursion, das Abbilden, Reduzieren und andere. Lesen Sie so viel Code wie möglich. Setzen Sie so viele Ideen wie möglich um. Wenn Sie Probleme haben, lesen Sie und lesen Sie.

Wenn Sie eine gute theoretische Referenz benötigen, um Haskell und andere funktionale Programmierparadigmen zu lernen, schauen Sie sich Folgendes an: Eine Einführung in die funktionale Programmierung durch Lambda Calculus, Greg Michaelson (online verfügbar). ... Es gibt noch andere ähnliche Bücher.

Hier ist ein (langer) Blog-Beitrag, der Motivation gibt, wie kategorietheoretische Ideen für die praktische Programmierung relevant sind: http://cdsmith.wordpress.com/2012/04/18/why-do-monads-matter/

Die Kategorietheorie ist ein sehr hoch entwickelter Zweig der Mathematik. Wenn Sie sie beherrschen, werden die meisten Ihrer früheren Lektionen vereinheitlicht, indem Sie sie zu Instanzen derselben abstrakten Objekte machen. Es ist also sehr nützlich und sehr intuitiv. Aber es ist riesig und breit und Sie werden in eine Menge neuer Konzepte geraten, die nicht einmal wissen, welches für Ihre Bedürfnisse geeignet ist und welches Sie überspringen sollten. Ihr zielgerichteter Ansatz erfordert also die Auswahl von Konzepten, ansonsten dauert das Erlernen zwangsläufig lange und ist in Wirklichkeit kein Selbstlernbereich.

Übrigens, ich schlage einen sehr guten Ausgangspunkt vor, um hier zu sein .