zero_coding - 3 years ago 135

Scala Question

I am reading Category Theory for Programmers, and I cannot figure out what exactly a category is.

Let's consider the

`Bool`

`Bool`

`True`

`False`

Recommended for you: Get network issues from **WhatsUp Gold**. **Not end users.**

Answer Source

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:

- taking each object (boolean expression) to its logical negation
- taking each arrow to a new arrow representing the same variable substitutions

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:

- the objects are types (like
`Bool`

,`Int`

, etc.) - the arrows are Haskell functions (like
`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`

). - composition is regular function composition

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`

:

- The "Discrete Boolean" category represents
`Bool`

as a plain mathematical set of two objects, "true" and "false", with no additional interesting features. - The "false -> true" category represents an ordering of boolean values,
`false < true`

, where each arrow represents the operator '<='. - The boolean expression category represents an evaluation model for simple boolean expressions.
`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.

Recommended from our users: **Dynamic Network Monitoring from WhatsUp Gold from IPSwitch**. ** Free Download**