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! 