I am reading Category Theory for Programmers, and I cannot figure out what exactly a category is.
Let's consider the Bool
type. Is Bool
a category and True
or False
are objects (inhabitants)?
One reason you're getting a lot of potentially confusing answers is that your question is a little like asking: "Let's consider a soccer ball. Is the soccer ball a 'game' with the black and white polygons its 'pieces'?"
The answer might be @arrowd's answer: "No, you've confused the game of soccer (Hask
) with its ball (Bool
), and the polygons (True
and False
) don't matter." Or, it might be @freestyle's answer: "Yes, we could certainly create a game using the soccer ball and assign one player to the black polygons and the other player the white polygons, but what would the rules be?" Or, it might be @Yuval Itzchakov's answer: "Formally, a 'game' is a collection of one or more players, zero or more pieces, and a set of rules such that, etc., etc."
So, let me add to the confusion with one more (very long) answer, but maybe it will answer your question a little more directly.
Instead of talking about the Haskell type Bool
, let's just talk about the abstract concept of boolean logic and the boolean values true and false. Can we form a category with the abstract values "true" and "false" as the objects?
The answer is definitely yes. In fact, we can form (infinitely) many such categories. All we need to do is explain what the "objects" are, what the "arrows" (sometimes called morphisms) are, and make sure that they obey the formal mathematical rules for categories.
Here is one category: Let the "objects" be "true" and "false", and let there be two "arrows":
true -> true
false -> false
Note: Don't confuse this ->
notation with Haskell functions. These arrows don't "mean" anything yet, they are just abstract connections between objects.
Now, I know this is a category because it includes both identity arrows (from an object to itself), and it satisfies the composition property which basically says that if I can follow two arrows from a -> b -> c
, then there must be a direct arrow a -> c
representing their "composition". (Again, when I write a -> b -> c
, I'm not talking about a function type here -- these are abstract arrows connecting a
to b
and then b
to c
.) Anyway, I don't have enough arrows to worry too much about composition for this category because I don't have any "paths" between different objects. I will call this the "Discrete Boolean" category. I agree that it is mostly useless, just like a game based on the polygons of a soccer ball would be pretty stupid.
Here's a slightly more interesting category. Let the objects be "true" and "false", and let the arrows be the two identity arrows above plus:
false -> true
This is a category, too. It has all the identity arrows, and it satisfies composition because, ignoring the identity arrows, the only interesting "path" I can follow is from "false" to "true", and there's nowhere else to go, so I still don't really have enough arrows to worry about the composition rule.
There are a couple more categories you could write down here. See if you can find one.
Unfortunately, these last two categories don't really have anything to do with the properties of boolean logic. It's true that false -> true
looks a little like a not
operation, but then how could we explain false -> false
or true -> true
, and why isn't true -> false
there, too?
Ultimately, we could just as easily have called these objects "foo" and "bar" or "A" and "B" or not even bothered to name them, and the categories would be just as valid. So, while technically these are categories with "true" and "false" as objects, they don't capture anything interesting about boolean logic.
Something I haven't mentioned yet is that categories can contain multiple, distinct arrows between two objects, so there could be two arrows from a
to b
. To differentiate them, I might give them names, like:
u : a -> b
v : a -> b
I could even have an arrow separate from the identity from b
to itself:
w : b -> b -- some non-identity arrow
The composition rule would have to be satisfied by all the different paths. So, because there's a path u : a -> b
and a path w : b -> b
(even though it doesn't "go" anywhere else), there would have to be an arrow representing the composition of u
followed by w
from a -> b
. Its value might be equal to "u" again, or it might be "v", or it might be some other arrow from a -> b
. Part of describing a category is explaining how all the arrows compose and demonstrating that they obey the category laws (the unit law and the associative law, but let's not worry about those laws here).
Armed with this knowledge, you can create an infinite number of boolean categories just by adding more arrows wherever you want and inventing any rules you'd like about how they should compose, subject to the category laws.
Here's a more interesting category that captures some of the "meaning" of boolean logic. It's kind of complicated to explain, so bear with me.
Let the objects be boolean expressions with zero or more boolean variables:
true
false
not x
x and y
(not (y or false)) and x
We'll consider expressions that are "always the same" to be the same object, so y or false
and y
are the same object, since no matter what the value of y
is, they have the same boolean value. That means that the last expression above could have been written (not y) and x
instead.
Let the arrows represent the act of setting zero or more boolean variables to specific values. We'll label these arrows with little annotations, so that the arrow {x=false,y=true}
represents the act of setting two variables as indicated. We'll assume that the settings are applied in order, so the arrow {x=false,x=true}
would have the same effect on an expression as {x=false}
, even though they're different arrows. That means that we have arrows like:
{x=false} : not x -> true
{x=true,y=true} : x and y -> true
We also have:
{x=false} : x and y -> false and y -- or just "false", the same thing
Technically, the two arrows labelled {x=false}
are different arrows. (They can't be the same arrow because they're arrows between different objects.) It's very common in category theory to use the same name for different arrows like this if they have the same "meaning" or "interpretation", like these ones do.
We'll define composition of arrows to be the act of applying the sequence of settings in the first arrow and then applying the settings from the second arrow, so the composition of:
{x=false}: x or y -> y and {y=true} : y -> true
is the arrow:
{x=false,y=true}: x or y -> true
This is a category. It has identity arrows for every expression, consisting of not setting any variables:
{} : true -> true
{} : not (x or y) and (u or v) -> not (x or y) and (u or v)
It defines composition for every pair of arrows, and the compositions obey the unit and associative laws (again, let's not worry about that detail here).
And, it represents a particular aspect of boolean logic, specifically the act of calculating the value of a boolean expression by substituting boolean values into variables.
It also has a somewhat interesting functor which we might call "Negate". I won't explain what a functor is here. I'll just say that Negate maps this category to itself by:
So, the arrow:
{a=false} : (not a) and b -> b
gets mapped by the Negate functor to:
{a=false} : not ((not a) and b) -> not b
or more simply, using the rules of boolean logic:
{a=false} : a or (not b) -> not b
which is a valid arrow in the original category.
This functor captures the idea that "negating a boolean expression" is equivalent to "negating its final result", or maybe more generally that the process of substituting variables in a negated expression has the same structure as doing it to the original expression. Maybe that's not too exciting, but this is just a long Stack Overflow answer, not a 500-page textbook on Category Theory, right?
Bool
as part of the Hask
categoryNow, let's switch from talking about abstract boolean categories to your specific question, whether the Bool
Haskell type is a category with objects True
and False
.
The answers above still apply, to the extent that this Haskell type can be used as a model of boolean logic.
However, when people talk about categories in Haskell, they are usually talking about a specific category Hask
where:
Bool
, Int
, etc.)f :: Int -> Double
). Finally, the Haskell syntax and our abstract category syntax coincide -- the Haskell function f
can be thought of as an arrow from the object Int
to the object Double
).If we are talking about this category, then the answer to your question is: no, in the Hask
category, Bool
is one of the objects, and the arrows are Haskell functions like:
id :: Bool -> Bool
not :: Bool -> Bool
(==0) :: Int -> Bool
foo :: Bool -> Int
foo b = if b then 10 else 15
To make things more complicated, the objects also include types of functions, so Bool -> Bool
is one of the objects. One example of an arrow that uses this object is:
and :: Bool -> (Bool -> Bool)
which is an arrow from the object Bool
to the object Bool -> Bool
.
In this scenario, True
and False
aren't part of the category. Haskell values for function types, like sqrt
or length
are part of the category because they're arrows, but True
and False
are non-function types, so we just leave them out of the definition.
Note that this last category, like the first categories we looked at, has absolutely nothing to do with boolean logic, even though Bool
is one of the objects. In fact, in this category, Bool
and Int
look about the same -- they're just two types that can have arrows leaving or entering them, and you'd never know that Bool
was about true and false or that Int
represented integers, if you were just looking at the Hask
category.
This is a fundamental aspect of category theory. You use a specific category to study a specific aspect of some system. Whether or not Bool
is a category or a part of category is sort of a vague question. The better question would be, "is this particular aspect of Bool
that I'm interest in something that can be represented as a useful category?"
The categories I gave above roughly correspond to these potentially interesting aspects of Bool
:
Bool
as a plain mathematical set of two objects, "true" and "false", with no additional interesting features.false < true
, where each arrow represents the operator '<='.Hask
represents the composition of functions whose input and output types may be a boolean type or a functional type involving boolean and other types.If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With