Dao of Functional Programming (Chapter 1: Clean State)

This would be an irregular series of posts on my new attempt to learn Category Theory. This time, it would be based on the book titled The Dao of Functional Programming written by Dr. Bartosz Milewski. Currently, I am doing it with assistance of NoteBookLM to understand the material better. So let’s start with the first chapter today and answer the question — What are objects and arrows in the world of category theory? An illustration generated by Copilot The current attempt is likely my third or fourth time learning category theory myself. In my previous attempts, I usually got lost in the later chapters. Hopefully, with the help of NotebookLM playing the role as a tutor, things get easier. Ah, how things have changed. Articles in the series would mostly be unstructured, there would be a very minimal amount of effort in storytelling..) Treat this as my study notes, and I welcome all feedback, insights, corrections etc. Notation Due to the limitation of Medium’s editor, for Mathematical symbols involving subscripts, say x ** 2 in Python, it would be written as x^2. In contrast, a subscript, would be written as x_2. Types and Functions The text advised against associating the concept of type and functions to concrete programming implementation. Therefore, please read the remainder of this article with a clean state of mind (now I understand the rationale behind the chapter’s name). In the context of category theory, a type can be considered as an object or a proposition. We can then assign names to each of them, e.g. a, b, c, or even familiar ones like Int, Bool, Double etc. The names are assigned purely to differentiate them from each other whenever applicable. The relationship between types, instead of what it is, is more essential. A relationship is established by connecting the types with arrows. Each arrow connects one source and one target type. A special case to consider is that the arrow can loop around, forming a connection with the type itself. Depending on the context or field of study, the arrows are named differently. We have been talking about types so far, so in this setting an arrow connecting types is called a function. When used in the context of category theory, an arrow connecting objects is called a morphism. In the world of logic, an arrow connecting propositions is called an entailment. A proposition is something that may be true. An implication is usually established with one premise mapping to an outcome or conclusion. The author uses the example “if wishes were horses, beggars would ride”. In this case, “wishes were horses” is the premise, and “beggars would ride” is the outcome. In this case, both premise and outcome are two different kinds of propositions. The implication, written in arrow form (wishes = horses) -> (beggars would ride), is therefore an entailment. The names of arrows can be used interchangeably, but the core idea is that they establish connections. Like what we did for types, we name arrows to differentiate them, as they may be more than one arrow between two types (objects, propositions). In this case, the arrow can be interpreted as a function f mapping values of type a to type b. Alternatively, it could also mean f is a proof that if a is true then b is also true. Yin and Yang I suppose types, and the corresponding functions, are considered as a specialized application of category theory. Each corresponding to a specialized object, and morphism respectively. We define objects by their connections An arrow is a proof/witness of the connection If there’s no arrow, there’s no proof, therefore the objects are considered disconnected. It is possible to have multiple arrows, hence many proofs. Sometimes there’s a single proof — a unique arrow Unique: even if we manage to find two arrows, they must be identical Initial Object An object with a unique outgoing arrow to every object, including itself. Unlike an initial node in a graph, an initial object can have incoming arrows, but in the context of the categories covered (types, logic), we are assuming no incoming arrow for initial objects. In Mathematics, often denoted by 0 The arrow from 0 to any object a is denoted by ¡ (or specifically ¡_a). Can be seen as a source of everything. As a type in Haskell, it is the Void type. As an initial type, there is also an arrow (function) from Void to itself. Hence, it can derive Void and everything else. All the unique outgoing arrows (functions) are all called absurd. In logic, it signifies logical falsehood/contradiction/counterfactual, written as F, False or ⊥. Again, the outgoing arrow characteristic means we can establish any entailment (proving) starting from false premises. ⊥ -> a, for every proposition a The earlier implication “If wishes were horses, beggars would ride” shows that, even the premise “wishes were horses” is false, but the arrow pointing to the proposition “beggars would ride” can still be

May 17, 2025 - 21:26

Dao of Functional Programming (Chapter 1: Clean State)

This would be an irregular series of posts on my new attempt to learn Category Theory. This time, it would be based on the book titled The Dao of Functional Programming written by Dr. Bartosz Milewski. Currently, I am doing it with assistance of NoteBookLM to understand the material better. So let’s start with the first chapter today and answer the question — What are objects and arrows in the world of category theory?

An illustration generated by Copilot

The current attempt is likely my third or fourth time learning category theory myself. In my previous attempts, I usually got lost in the later chapters. Hopefully, with the help of NotebookLM playing the role as a tutor, things get easier.

Ah, how things have changed.

Articles in the series would mostly be unstructured, there would be a very minimal amount of effort in storytelling ..) Treat this as my study notes, and I welcome all feedback, insights, corrections etc.

Notation

Due to the limitation of Medium’s editor, for Mathematical symbols involving subscripts, say x ** 2 in Python, it would be written as x^2. In contrast, a subscript, would be written as x_2.

Types and Functions

The text advised against associating the concept of type and functions to concrete programming implementation. Therefore, please read the remainder of this article with a clean state of mind (now I understand the rationale behind the chapter’s name).

In the context of category theory, a type can be considered as an object or a proposition.
We can then assign names to each of them, e.g. a, b, c, or even familiar ones like Int, Bool, Double etc.
The names are assigned purely to differentiate them from each other whenever applicable.
The relationship between types, instead of what it is, is more essential.
A relationship is established by connecting the types with arrows.
Each arrow connects one source and one target type.
A special case to consider is that the arrow can loop around, forming a connection with the type itself.
Depending on the context or field of study, the arrows are named differently. We have been talking about types so far, so in this setting an arrow connecting types is called a function.
When used in the context of category theory, an arrow connecting objects is called a morphism.
In the world of logic, an arrow connecting propositions is called an entailment.
A proposition is something that may be true.
An implication is usually established with one premise mapping to an outcome or conclusion. The author uses the example “if wishes were horses, beggars would ride”. In this case, “wishes were horses” is the premise, and “beggars would ride” is the outcome. In this case, both premise and outcome are two different kinds of propositions. The implication, written in arrow form (wishes = horses) -> (beggars would ride), is therefore an entailment.
The names of arrows can be used interchangeably, but the core idea is that they establish connections.
Like what we did for types, we name arrows to differentiate them, as they may be more than one arrow between two types (objects, propositions).

In this case, the arrow can be interpreted as a function f mapping values of type a to type b.
Alternatively, it could also mean f is a proof that if a is true then b is also true.

Yin and Yang

I suppose types, and the corresponding functions, are considered as a specialized application of category theory. Each corresponding to a specialized object, and morphism respectively.

We define objects by their connections
An arrow is a proof/witness of the connection
If there’s no arrow, there’s no proof, therefore the objects are considered disconnected.
It is possible to have multiple arrows, hence many proofs.
Sometimes there’s a single proof — a unique arrow
Unique: even if we manage to find two arrows, they must be identical

Initial Object

An object with a unique outgoing arrow to every object, including itself.
Unlike an initial node in a graph, an initial object can have incoming arrows, but in the context of the categories covered (types, logic), we are assuming no incoming arrow for initial objects.
In Mathematics, often denoted by 0
The arrow from 0 to any object a is denoted by ¡ (or specifically ¡_a).
Can be seen as a source of everything.
As a type in Haskell, it is the Void type.
As an initial type, there is also an arrow (function) from Void to itself. Hence, it can derive Void and everything else. All the unique outgoing arrows (functions) are all called absurd.
In logic, it signifies logical falsehood/contradiction/counterfactual, written as F, False or ⊥.
Again, the outgoing arrow characteristic means we can establish any entailment (proving) starting from false premises. ⊥ -> a, for every proposition a
The earlier implication “If wishes were horses, beggars would ride” shows that, even the premise “wishes were horses” is false, but the arrow pointing to the proposition “beggars would ride” can still be drawn.

Terminal Object

An object with a unique incoming arrow from every object
Unlike a terminal node in a graph in a graph, a terminal object can have outgoing arrows.
In Mathematics, often denoted by 1
The arrow from any object a to 1 is denoted by ! (or specifically !_a).
Can be seen as an object that unites everything.
As a type in Haskell, it is the Unit type, denoted by ().
In logic, it signifies the ultimate truth, written as T, True or ⊤.
The incoming arrow characteristic means any proposition can entail True, regardless what they are. a -> ⊤, for every proposition a

| Category theory | Haskell | Logic |
|-------------------|----------|-------------|
| object | type | proposition |
| morphism | function | entailment |
| initial object, 0 | Void | ⊥ |
| terminal object | () | ⊤ |

Elements

Structure

Objects are primitive and cannot be broken down into smaller components
Structure: arrows pointing at the object (incoming arrows)
We can probe an object with arrows.
Assumption: For programming and logic, we want our initial object to have no structure, therefore no incoming arrow (aside from the self-looping arrow).
Void and False therefore have no structure.
Terminal object has only one way of probing it from any direction into the object, hence having the simplest structure.
Considered as the indivisible point: a single, uniform target reached by a unique connection from anywhere
Only property is that it exists, proved by the existence arrow from any other object (recall proof: having an arrow connecting objects).

Probing other objects

Terminal object is simple, can use it to probe other more complex objects
If there are more than one arrow from the terminal object to an object a, then a has some structure.
Each arrow means a way to look at an object, having multiple arrows means more than a way of looking at it.
Now we know a terminal project behaves like a (indivisible) point, can visualize each arrow from it as picking another point or element of its target (another object)

Global Element

As mentioned previously, initial object can have incoming arrows. However, in the context of the Cartesian closed categories covered, incoming arrows are not allowed.

The arrow x is defined as a (global) element of_ _a.
The notation in type theory: x : A, x is of type A
The Haskell counterpart (use double colon notation): x :: A
Haskell uses capitalized names for concrete types such as Void, Int, Double etc. In the example, it is A
Lowercased names for type variable, in the example it is x
The example defined x as a term of type A
Categorically, we interpret it as an arrow x : 1 -> A, which is a global element of A
In logic, x is the proof of A because it corresponds to the implication (a type of entailment, or an arrow) T -> A (if T is true then A is true)
There may be multiple proofs of A (many arrows from T to A)
Initial object like Void has no incoming arrow including from the Terminal, therefore Void has no elements.
Void is therefore considered empty.
Terminal object has only one unique arrow coming from itself 1 -> 1
Due to the unique self-pointing arrow, it is sometimes called a singleton

The Object of Arrows

Arrows between two objects form a set (with some exceptions, but I am ignoring that for now)
In programming we talk about the type of functions from a to b, in Haskell it would be f :: a -> b
Side note: In Python it would be f: Callable[[a], [b]]
Meaning: f is of the type “function from a to b” (a -> b)
So if a -> b is a type, then there would be an object that represents the set of arrows (functions) from a to b.
Further steps to define this object of arrows to be covered in later chapters.
In addition to the set of arrows, there is an object of arrows.
Recall, an element of an object is defined as an arrow from a terminal object (Unit) to a target object.
Therefore, in this case, an element of the object b^a is an arrow from the terminal object to b^a, and this arrow corresponds to a function of type a -> b
In category theory, the object of arrows is called an exponential, and is written as b^a (source object in the exponent)
Therefore f :: a -> b, written as an element of an object of arrows is as shown below.

One thing to note is that if there is no arrow connecting a and b, then the set of arrow a -> b is empty, and we will fail to find the global element arrow (prove) between the terminal object and corresponding b^a object.
For example, in programming, if there is no way to map an Int to Bool, then the set of the function Int -> Bool is empty, and there will be no elements in the corresponding Int^Bool object.
In logic, an arrow A -> B is an implication, it states the fact that “if A then B”.
Therefore, the exponential object B^A, is a proposition in the context of the following expression:

Recall in logic T -> A means if T is true, then the proposition A is True.
Also recall an arrow is a proof where two objects are connected.
So the global element x means the entailment from A to B exists, and is also valid.
Therefore when we revisit the statement “If wishes were horses, beggars would ride” as a proposition (an object), then we should be able to prove the arrow from A (wishes were horses) to B (beggars would ride).
However, in the case where “wishes = horses” cannot be proven as there is no arrow from the ultimate truth to the proposition. Therefore, the original implication is valid, but the premise cannot be found, hence beggars would not ride.

Closing thoughts

Understanding the object of arrows in the context of logic takes up a lot more time than I initially expected, but I am quite happy I finally managed to complete the article. One piece of advice I would share is try to learn as if you have not done much Mathematics before. Prior knowledge in other fields has only brought confusion so far. Anyway as this is going to be irregular, I will continue when I have the time.

This article was written with assistance from Gemini, a large language model by Google. Gemini provided editorial help, fixing language errors and checking for article flow. However, the code and voice are entirely my own. If you’d like to collaborate or discuss job opportunities, please connect with me on LinkedIn or via Medium.