Category Theory in Programming

General
,
1

The full tutorial is here CTP.

In this tutorial, I explore the applications of category theory in programming, using Racket to represent abstract mathematical concepts. The completed sections introduce categories, functors, and natural transformations, demonstrating how these ideas map into programming constructs with practical code examples. This work aims to help programmers understand system design from a mathematical perspective, building a foundation that progresses from basic structures to advanced abstractions.

The motivation for this tutorial stems from my own journey of learning category theory. Initially, I often wondered what category theory meant in the context of programming but struggled to find answers. This changed when I encountered @countvajhula's Qi project, which amazed me with its ability to align category theory concepts with programming constructs. Using qi, one can program in a Cartesian closed category style, distinct from the lambda calculus approach. This inspired me to abstract the concept of Category much like how one abstracts pair, enabling the use of programming examples to further explore category theory.

As someone without a formal mathematics background, I have self-taught category theory and written this book to share the connections I've discovered between programming and category theory. My hope is to inspire programmers to think about and solve problems, as well as design systems, through the lens of category theory. However, as a non-mathematician, I acknowledge that there may be inaccuracies or a lack of rigor in some areas, and I warmly welcome feedback to improve this work.

8 Likes
2

This looks amazing! :star_struck:

(Btw, this probably needs some kind of tag to indicate it’s part of the advent calendar. What would you advise @spdegabrielle ?)

1 Like
3

I've added the tag advent-2024

Thank you @NoahStoryM

Stephen
:christmas_tree:

3 Likes
4

Motivation Behind CTP

The CTP project was inspired by my exploration of the Qi project, which offers a rich set of operators for composing functions. Qi's core operators, such as n>, ==, -<, and ><, revolve around values, and @countvajhula once proposed the idea of complementary operators (like <>) without fully defining their semantics (source).

When I started using Qi, these operators—especially values—reminded me of category theory's product in the Set category. Specifically, values seemed to correspond to the Cartesian product of Set.

For example:

  • The Qi operator -< aligns with the pairing and ==* aligns with the product in category theory:
  f : A -> X
  g : A -> Y
  h : B -> Z
  (-<  f g) : A -> X Ă— Y
  (==* g h) : A Ă— B -> Y Ă— Z

Similarly, Qi inspired me to think about sums in Set (disjoint unions or tagged unions). For example, X = {x}, Y = {y}, then X + Y = {(x, 0), (y, 0)}. This led to defining dual operators for Qi:

  • >- corresponds to copairing and ==+ corresponds to coproduct:
  f : X -> A
  g : Y -> A
  h : Z -> B
  (>-  f g) : X + Y -> A
  (==+ g h) : Y + Z -> A + B

This realization led me to re-examine examples of Cartesian closed categories (CCCs) in Category Theory for Computing Science using Qi (source). To my surprise, Qi's operators aligned naturally with the mathematical constructs.

As a programmer, the functional programming languages ​​I have encountered are all based on lambda calculus, and I had never heard of CCC before. Now I know another programming style that is centered on functions (more precisely, morphisms).

This exploration of Qi also made me think about its type system. In Typed Racket, the handling of values is limited, restricting the use of compose, which is central to Qi. I think Typed Racket's type and contract systems could be extended using ideas from limits in category theory. This could enable a more robust and expressive system for composing functions.

On the other hand, Qi also aims to enable flow-oriented programming (source). In my understand, each Qi instance could represent a category, its flows represent morphisms in that category. Using functors, we could establish relationships between different Qi instances, leading to natural transformations and even higher abstractions like 2-categories.

I've experimented with code drafts to explore these deeper connections between category theory and programming (source), and the results have been fascinating! I think this way of programming can be called morphism-oriented programming.

Why Write CTP?

CTP is not a comprehensive textbook but more of a collection of mathematical notes inspired by my programming experiments. As a programmer without formal mathematical training, I use programming to better understand category theory concepts. Writing this book has been an iterative process, focusing on foundational topics like categories, functors, and natural transformations to ensure a solid understanding before tackling more abstract ideas.

Unlike traditional category theory resources that use examples from other mathematical fields, I rely exclusively on programming examples. The goal is to demonstrate that programmers can understand the basics of category theory using only familiar programming constructs. By knowing what categories, functors, and natural transformations are and how to abstract them in code, programmers can independently explore deeper aspects of category theory, which is my main motivation for releasing this work-in-progress at the moment.

While the content is still rough, I hope it will inspire programmers to consider category theory as a new way of thinking about designing systems and solving problems, just like I did with Qi! :stuck_out_tongue:

3 Likes