Incorporates strong typing over predicate logic programming, and, conversely, incorporates predicate logic programming into strongly typed functional languages. The style of predicate logic is from Prolog; the strongly typed functional language is Haskell.
An introduction to Category Theory for Java Programmers
Okay, folks, here it is, the whole shooting match: the answer to the question of life, the universe and everything! The silver bullet, the whole enchilada, the ... the ... raison d'être, the sine qua non.
What am I talking about? I'm talking about categories, of course, because that's the answer to every question: how do I sort a list? how do I save this object to the database? how do I compute the solution to this problem? does everything look like a nail when I have a hammer?
Yes, yes, yes, and yes.
Of course, to make bold statements like these, I must back them up — unless I'm Shishir — so let's back away from the hype and enthusiasm and look first at what categories are, and then we'll look at various kinds of categories and then how we can use them in everyday programming tasks and see where they make things easier or simpler for us to tackle.
Okay, here we go.
Now, we're going to get really technical here (not really, ... so chill), and I'm going to use really technical terms, like the word 'thing.' I'm going to use the word 'thing' a lot, so if you have any questions on that, just ask.
You: "Uh, geophf, what's a 'thing'?"
Me: Glad you asked. A 'thing' is a thing. Any more questions?
No? Moving on.
So, a category is a collection of things. That's (nearly) all it is. The thing is, the category is the collection of any, all, and every thing of the kind of thing that the category is.
Put another way, the category of natural numbers is the entire universe, if the universe started at 0, and then had 1, 2, 3, ... and on.
Sound a lot like a set or a class of things, right?
Sure, but a category has a certain set of rules about it. Not only is it a collection of all things of that type of thing (we call them 'objects'), but it also has another set of things associated with that, and these things are called 'morphisms' or 'arrows.'
Now, 'morphisms' (I'll call them 'arrows,' from now on, because if you're in a conversation with your friendies at a cocktail party and you mention categories have morphisms, they'll say, 'what are morphisms?' and you'll explain that, and then they'll say, 'well, that's all Greek to me,' ... and they'll be right! But the twentieth time saying 'yes, you're right! It is Greek!' will get kind of old, so I'll just stick with the word 'arrows,' because sticking with simpler terms is (slightly) less intimidating) are simply things that take a thing and give you another thing in a (perhaps different) category.
So, for example, a morphism (or arrow) that takes a natural number and gives you money is this:
change :: ℕ→ $
And so if I get change for my natural number:
in Cat$. And I'll be feeling pretty good, because I'll just scale up the logarithm to cover any expenses I may have incurred for publishing this article. AND to buy a cup of coffee at Caribou Café.
So, don't let anyone tell you Categories are good for nothing, because Categories and $6.57 in your pocket will buy you a cup of flavored espresso drink ... or, mmmm! a French press!
So, that's an example of an arrow that takes an object from one category and gives you an object in another one.
Arrows don't (necessarily) have to move objects from one category to a different one. If I have:
succ :: ℕ→ℕ
And I do the same thing:
which is an object in the same category of natural numbers, which we write Catℕ
Well, all categories have one special requirement for their arrows. There must be, for the objects in the category, an arrow, call the identity arrow (labeled 1C replacing the C with the category we're in) that takes an object and gives you back the exact same object. We, in lowly programming languages that don't allow you to call functions '1C' call this arrow 'id.' So:
id 1 = 1
Now, the 'id' arrow seems rather pointless, but it's needed in actual use quite often, and is essential because for a category to be a category it has to obey three laws:
The Three Laws of Categories
For any category, C, the following three laws hold:
1. for all p: id ⋅ p = p (left identity)
2. for all p: p ⋅ id = p (right identity)
3. for all p, q, and r: (p ⋅ q) ⋅ r = p ⋅ (q ⋅ r)
Okay, we have some terms/symbols we need to explain here.
The '⋅' means 'composition.' and composition is when we take one object and 'compose' it with another one. What does it mean to compose objects?
Well, that definition depends on which category you're in, but if you're in the category of morphisms, then composition is ... erhm, well: composition.
or, put it this way:
(g ⋅ f) x
means in plain English:
'Take the object x, apply the function g to it, then take that result and apply f to that.'
f ( g ( x )) = (g ⋅ f) x
Okay, that defines '⋅' but what does '=' mean?
You: Huh? Everybody knows what '=' means, it means 'equals,' obviously.
Me: Yes, but what does 'equals' mean?
See, in an unit category, like Catℕ, equivalence is easy: 1 = 1, 2 = 2, and 2 ≠ 3, etc.
But objects can be anything in a category, so, for example, you could be in the category of arrows, or (equivalently) the category of combinators ... or even the category of categories, ... you can take the abstraction as far as you'd like.
(Historical note: category theory was originally known (lovably?) as 'abstract nonsense.')
So, if you're in some category where it's difficult to eyeball equivalence, what does '=' become? I mean, it's easy to see 1 = 1, but in the category of combinators does
K = S(SKKK)(IK)K ?
Well, in fact, it does, if we take '=' not be 'equals' as in 'exactly the same thing as' but take 'equals' to be 'isomorphic.'
There's that root word 'morph,' again.
What does 'isomorphic' mean?
(You see, if you took your ancient Greek, you'd be so far ahead of the curve here. If this were the late 1930s, we wouldn't be having this conversation, because the (American) English language had many more words with roots in Greek than what they do today, which is a sad loss for our language today, but not the topic of this article.)
Well, 'morphism' is a thing that changes a thing into another thing. 'Morph' means 'ch-ch-ch-changes!'
So, 'isomorphic' means a thing that changes a thing into the same thing: 'iso' means 'same.'
Just remember the words to the song:
"My grandma said to your grandma, Iso, Iso all day!"
And you'll do fine with isomorphisms, because when you ask people: "How's it going?" they invariably say: "Same ol', same ol'," am I right? And that's the same ('isomorphic to') as saying: "Iso, iso all day."
So, well, how do we test for '=' with isomorphisms if we can't eyeball it any more?
That's where the 'for all' comes in.
What we do is that if we take every object in the category, and we put into a morphism, then the statement of isomorphism holds if every resulting object on the left hand side (lhs) of the isomophism is the same ('has the same shape') as every resulting object on the right hand side (rhs) of the isomorphism.
So, looking at rule 1 above ('left identity') which was, as you recall:
id ⋅ p = p
Then an example is:
id ⋅ succ = succ
Let's test that:
lhs: (id ⋅ succ) 5 = succ (id 5) = succ 5 = 6
rhs: succ 5 = 6
That one holds. How about:
lhs: (id ⋅ succ) 42 = succ (id 42) = succ 42 = 43
rhs: succ 42 = 43
There we go, we have two objects that verify our rule. Now all we have to do is to verify the rest of the objects in Catℕ
Exercise 1: verify left identity holds for succ for all objects in Catℕ
Done with that? Good. No? Here's a hint: use induction.
Exercise 2: verify that right identity holds for succ for some objects in Catℕ
Categories in Java
Well, the above was a high-level introduction to Categories, but how do we get categories into Java?
That's easy as 3.14159...! (π to your friendies) We simply define it:
The Java definition is short and sweet: a Category is a thing that has an identity morphism (id()) and can compose (from the left function to the right function, because that's how I like to roll, from the left to the right) two categories to get a third, particularly:
Cat(A→B) ⋅ Cat(B→C) = Cat(A→C)
which mirrors the dual of how we defined composition above.
Now, we can id() and composeLR() categories until we're blue in the face, and it's all very pretty to look at, but what's it good for?
Well, it's good for moving objects (and transforming them) from one category to another, and that explanation sounds very dry, but there's a magic going on here, because this very simple definition gives us every and anything, and we need simply fit what we're working with into category theory, following the rules as we go, and we have a framework that has some well-understood supporting machinery to it as well as the rigor of strong mathematical proofs. This means that when you put something into a category, you have confidence that that something obeys the rules of categories.
Now, what that means for us on the Planet Earth, slinging Java code to get this next sprint done in our Agile project will be the topic of the articles following this one, where we will define some specialized categories and explore some things already explored in mathematics, such as monads and comonads and how these things allow us to do logic programming or data flow or workflow analysis or whatever you want to call it so we can get our jobs done, in Java, and be (provably) sure what we say we're doing is what we've actually done.