Understanding category theory and its practical applications

Note on the obvious: these thoughts represent my original state of mind when this post was first made, and do not necessarily reflect my current understanding. This OP is left unmodified for reference purposes.

Introduction

Various logics and mathematics, such as set theory, predicate calculus, arithmetic, et. al. were relatively intuitive and came easy to grasp when I learned them. Additionally, they came with their obvious applications, not just to problems in the real world, but also to programming and programming languages. It is easy to see the higher level of abstraction that comes from using these as opposed to a computation-oriented programming language.

Predicate calculus, in particular, is a powerful language suited to various boons from a programmer's perspective, including arbitrary constraint qualification as a means to better aspect-oriented programming. However, I have not been able to identify any such gains from category theory. I can't see how it is any better than anything else.

Note: My understanding of category theory is very shoddy, so using lots of category-theoretic terminology may obscure my understanding of your answer--being moderate will help. From what I gather, a morphism seems to be a transformation (possibly represented by one or more functions), and the objects in a category could be represented as a set. But if I am right, then how is category theory any better than just simply using functions, relations, and set theory?

I can never be sure if my understanding of category theory heads in the right direction, however, because nobody has tried to define category theory in a non-category-theoretic way, which has left me to wallow in the misery of trying to understand these concepts by googling for and reading all the non-terminating, mutually recursive definitions of such concepts. If all these proportedly wonderful concepts and discoveries made by scientists go over everyone else's heads, then how is anyone going to benefit? These concepts might as well have never been discovered, in such a case.

Prime points to address:

  1. Is it any better than set theory and predicate calculus, as far as abstraction is concerned? If so, how? What kinds of inferrable details does it abstract away (if it were to be employed within a programming language)?
  2. Is there a simple real-world metaphor to categories? I wonder how similar category theory is to mainstream-industry OOP.
  3. (Important!) How is it used to mathmatically/logically model story problems (like the kind you solve in a math class)? Can anyone produce story problems that can elegantly be solved using category theory, or that demonstrate the effectiveness of its paradigm for mathematical/logical modeling?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Try reading "Conceptual Math"

After getting stuck on page 44 of Goldblatt's Topoi I purchased
Conceptual Math" by Lawvere and Schanuel
This is truly a "category theory for dummies" book, but I found myself in suitably deep water pretty quickly, but with lots of simple real-world examples to allow me to find my way home. I find that there are a lot of seemingly fuzzy issues in CS which are clarified by CT, and I find myself more and more using CT concepts in my real-world design and analysis.

Thanks!

This book clarifies it so much! I wasn't far off the mark after all!

Things noted

It is apparent that category theory is essentially the same thing as objects and the relations between them, which is the same thing as functions. I quote the given book:

Other words that mean the same as function and map are transformation, operator, morphism, and functional; the idea is so important that it has been rediscovered and renamed in many different contexts." (page 22)

And let me add to this list, "relation" and "indirection".

I suppose, then, a prime advantage of category theory is that it explicitly and formally denotes a previously informal paradigm, bringing it into our conciousness, in which the hidden order, structure, correspondence, and symmetry of complex systems of relations are brought to the surface.

One could also say that category theory also provides a suitable organizational framework for analogies and metaphors.

or...

Analogies and metaphors can be made implicit, even emergent if conceptual 'mappings' are treated as categories, by virtue that composition is associative.

An example:
grizzly bears can be thought of as being mapped maybe to ferocity and possibly strength, strength may be mappable to the idea of strong things, and strong things may map to steel bars. So one making a metaphor, grizzly's are the steel bars of the mountain, could be viewed as making an association of f: grizzly->strength, g: strength->strong things; h: strong things->steel bars such that h.g.f which equals (h.g).f = h.(g.f). which seems trivial in this small example, but blow the #functions to 100, 1000, 1000000. The point groups of composed functions could be partially triggered, results 'combined and it wouldn't matter' so let h.g = a; then a.f. The point is there is no 'hardwiring' of metaphors; they are naturally arising just from using categories.

A metaphor for categories and mappings

Winheim asks "Is there a simple real-world metaphor to categories?"

Well, ironically, metaphors are themselves excellent places to start. Metaphors are mappings between words, concepts, stories. The metaphor of one's life as a journey down a road, a path. (Technically, one might look at one's life and its events and compare it to a journey and its events and see a "mapping between these mappings," a functor.)

As to why category theory has been "more useful" (in parts of mathematics and computer science) than set theory has been, this is because sets are sort of "impoverished." They deliberately lack structure, being just bags or collections of points, with no implied connection between the points and relatively few tools for discussing how the collections may change (for example, over time, one of our most important "journey-like" mappings).

For a really simple, real world example, consider a lawnmower. When out of gas/petrol, it needs to be refueled. The category of empty lawnmowers has an arrow/mapping/morphism to the category of full lawnmowers. Here the focus is more on the _process_ of mapping one category into another, or mapping one collection of things into another collection.

It's been said that category theory places mappings/arrows on a fully-equal footing with objects/points/things.

Now back to the lawnmower example. A child walks out to watch his father mowing the lawn. The lawmower runs out of gas. The child says "Daddy, I think the lawnmower needs a drink."

What the child is doing is using his own set of mappings, from thirsty to not thirsty, to metaphorize the process of fueling the lawnmower. There's a mapping between these mappings, a functor. (I happen to think this categorical way of thinking is immensely important for how we understand the world, how we might program artificial intelligences, and so on. Even more than "design patterns," I think we and other creatures chunk the world into pieces we can understand by finding the mappings and functors and so on which allow us to grok the world. We are, I think, category theory engines.)

In an important sense, compilers for various languages map categories (source code, for example) into other categories (executable code). The way C++ does this mapping may be different from the way Haskell does it, so there are functorial relations between the mappings. (And so on, for many levels of computer programming. Category theory played a crucial role in the 60s and 70s in the work of Peter Landin, Dana Scott, and others.)

Category theory is about a lot more than just these kinds of simple mappings. In particular, MacLane and Eilenberg found that many of the things they were seeing in algebraic topology, circa 1940, had these same kinds of "very similar mappings," and "mappings between mappings." They abstracted out the general similarties (the metaphors) and gave us the language of categories, functors, and natural transformations.

(Which are sort of like mappings between functors, but with interesting "dual" properties. MacLane later said that the stuff about categories and functors would've been just a notational invention, and sort of banal (my term), had it not been for natural transformations, which is where things get really interesting and useful in calculations about categories.)

The Lawvere and Schanuel book is excellent. I wish the "New Math" had really taken hold and I had been taught out of a book like this when I was still in high school. But the L & S book never has time to get too much beyond the "mappings and functors" level. Stuff about natural transformations needs examples for linear algebra, for example.

Or examples from Haskell :-). (The world of programming is rife with category theory ideas, from endofunctors to monads to zippers. Needless to say, the connection between category theory and functional programming is an especially tight and yet rich one.)

I hope this helps. Perhaps I am strange in this regard, but I think good programmers need more of this kind of mathematics than they do of calculus or numeric methods.

Slogan? "Conceptual mathematics IS programming."

--Tim May

That explains it very nicely,

thanks!

As to why category theory has been "more useful" (in parts of mathematics and computer science) than set theory has been, this is because sets are sort of "impoverished." They deliberately lack structure, being just bags or collections of points, with no implied connection between the points and relatively few tools for discussing how the collections may change (for example, over time, one of our most important "journey-like" mappings).

And that's where relations, functions, and predicates come in. Basically, then, category theory is a refined integration of both set theory and the world of functions.

. . .

So, I suppose natural transformations or functors can be used as a way to model dynamic (lower-order) morphisms.

. . .

So, I guess I need to figure out if category theory, compared to a higher-order predicate logic, would make both a better programming language and a better database model.

. . .

Thanks again.

Both more and less

And that's where relations, functions, and predicates come in. Basically, then, category theory is a refined integration of both set theory and the world of functions

In some sense, yes, but it can also be seen as more primitive than set theory with functions. Part of the usefulness fo category theory is in its abstraction; arrows (or morphisms, whichever name you prefer) are taken as primitives: we don't say what they are, simply that they exist and have certain properties. Certainly, if you think in terms of sets, then arrows look rather like functions, but that doesn't mean that arrows are functions, simply that they can be viewed that way in some contexts. If we are interested in the category of open sets in a topological space, then arrows are inclusion relations, not functions. In other contexts they can be more bizarre still. You don't need to think in terms of sets and functions to be able to use category theory, and in many ways that is where it's power comes from.

A more useful way to think about category theory compared to set theory is to view it as a kind of inversion of reasoning. In set theory everything is built up, and we understand objects by seeing what they are made of -- picking apart their internals. We relate two objects by comparing what they are made of. Category theory turns that on its head and takes relationships between objects as primitive. From CT's point of view objects are opaque; we understand an object not by peeking inside at it's internal structure, as we would if we were using set theoretic thinking, but rather by examining how the object relates to other objects.

I understand that might be high level and abstract, but I'm a mathematician, so I can't give you CS examples very easily.

ADTs

I understand that might be high level and abstract, but I'm a mathematician, so I can't give you CS examples very easily.

The obvious CS analogy is an abstract data type. For example, a stack is some type 'S a' where we have operations:
empty : S a
push : a -> S a -> S a
pop : S a -> 1+S a
top : S a -> 1+a

with equations like:
top empty = pop empty = inl ()
pop (push x xs) = inr xs
top (push x xs) = inr x

Now any implementation of "stacks" that satisfies the above is acceptable.

Great post

Thanks for that explanation.

If perception's your game...

I think we and other creatures chunk the world into pieces we can understand by finding the mappings and functors and so on which allow us to grok the world. We are, I think, category theory engines.

If I'm reading you correctly, when it comes to how we perceive the world, psychologist J.J. Gibson called these "affordances." Google's telling me that the AI set's already delved into what affordance theory means for artificial intelligence, but I can't speak to much beyond that because my brain would melt.

Affordances, Readiness-to-Hand, and Higher-Level Languages

Thank you for bringing up the issue of "affordances." This whole area is closely related to Heidegger's approach to being, being in the world, readiness to hand, thrownness, and to ontology. (The links to programming are not yet clear, or at least do not seem to be widely used by programmers. Even in AI. I think they will be, eventually.)

A very readable paper on the Heidegger/Gibson point of view is by two psychologists, Zahorik and Jenison:

http://wavelet.psych.wisc.edu/Zahorik_Jenison.pdf

This impinges on data bases and object ontologies, as this quote hints at:

"Instead of researchers building an artificial intelligence system in which properties of objects are construed as sets of atomistic, determinate features (the rationalist procedure), things in the world are instead incorporated into the system, or formalized according to their potentials for action/intereaction with the system itself, their "readiness-to-hand." A basketball is not represented by the features _round_, _orange_, and _rubber_, but instead is viewed for its _throwabiity_, its _rollability_, or its _bouncability_ by the system." (p. 7)

In Gibson/Norman terms, an actor encountering a basketball is more reactive, more _interested_ in, the latter features and not the purely physical or chemical properties.

I suspect this is the direction AI programming, and even Web ontologies (Web 3.0?), aka "the semantic Web" (Berners-Lee, etc.) will need to go. In terms of our kind of languages, this suggests:

-- much more than just "declarative" (a la logic or functional language)

-- more _process_ oriented (mappings) than _object_ oriented

-- categories, functors, and even n-categories

Languages which support very rich kinds of mappings/relations seem to have big advantages over even languages with "logic" (at the first order predicate calculus level) and "object" support.

One of the flaws in CYC is, I think, the almost completely "flat" data base of a vast number of logical assertions ("a basketball is round") without higher-level mappings of the sort that category theory may help to provide. Searle's "Chinese room" is another way to look at this.

To make a probably obvious point, the functional programming point of view may turn out to be much more useful than the object-oriented point of view, probably long anticipated by guys like McCarthy and Steele and all.

--Tim May

Also recommended is

Also recommended is Haugeland's 1995 Mind Embodied and Embedded (which can be found in his collection Having Thought).

The problem with

The problem with situatedness is that it can't be just defined "up to isomorphism". It is the opposite of a spiritual disembodied quality. Replacing object entities by relationships and naive facts about things by the way they might transform doesn't buy you much in this respect.

It raises the level of abstraction but I'm not sure it's just a revival of the old Bourbaki delusion: create an abstract framework ( burocracy ) and believe that it captures all relevant future efforts. Those will be just examples that fill gaps as special cases. In software development this delusion is expressed by the term "frameworkitis" that will always be attacked by more lightweight, situated and contextualized solutions that do not pretend to require states of a higher mind or other esoterica. I admit though it's hard to draw the lines between what is usefull and what is bogus - as always.

To make a probably obvious point, the functional programming point of view may turn out to be much more useful than the object-oriented point of view, probably long anticipated by guys like McCarthy and Steele and all.

I like that you finally talk about usefullness because this puts things on the ground. Otherwise I suspect some people will dismiss the usefullness of anything that wasn't built with the right attitude. So it might not bring anything further.

Connections

This direction sounds to me like it might be related to the Event Calculus, or to Transaction Logic. The Discrete Event Calculus Reasoner is a nice implementation of, of course, the Discrete Event Calculus and FLORA-2 is a very nice implementation of a combination of F-Logic, HiLog, and Transaction Logic in XSB Prolog, which can sit on top of any ODBC-compliant database. I'm quite impressed.

It seems very likely to me that, long term, what you're referring to will end up being an application of The Basic Intuitionistic Logic of Proofs (PDF) or something derived from it. A set of slides, also in PDF, giving a good overview can be found here. Related foundational papers would seem to include Explicit Provability and Constructive Semantics (PS) and Reflective lambda-calculus (PS). Note well: my impression derives from a regrettably superficial reading stemming from my near absolute ignorance of progress in logic (or, more accurately, logic education as a subset of computer science education in America) since the mid-1980's.

Ob. tie-in to LtU: I discovered the work on iBLP and related topics as a consequence of googling "constructive quantifiers" after Tim Sweeney used the phrase in a critique of A Very Modal Model of a Modern, Major, General Type System in private correspondence. To the extent that I understand Tim's critique at all, my interpretation is that he believes the type system in VMMMMGTS wouldn't be appropriate for a high-level language, but might be for the TILs and TALs that it is aimed at. In any case, I don't think it's entirely coincidental that "The technique... reduces mainly to defining a Kripke semantics of the Gödel-Löb logic of provability." (VMMMMGTS) and:

Brouwer-Heyting-Kolmogorov: a sentence is true if it has a proof, whereas proofs satisfy the following BHK conditions:

  • A proof of AB consists of a proof of A and a proof of B,
  • A proof of AB is given by presenting either a proof of A or a proof of B,
  • A proof of AB is a construction which, given a proof of A returns a proof of B,
  • Absurdity ⊥ is a proposition which has no proof, ¬A is A→⊥

...
Major models for intuitionistic logic
...
8. Kripke models (1965)
...
None solves the original BHK problem!
...

  • Big distraction and big help: Provability logic with []F ~ Provable(F) is modal system GL (Gödel-Löb—my emphasis) incompatible with S4. Though applications of GL have been mostly limited to Proof Theory, its mathematics provided a solid background for the solution of Gödel's problem.

...
The Logic of Proofs LP
...
Major features that differ LP from CL/λ-calculus.

  • Polymorphism. Operation "+" yields multiple types, i.e. multi-conclusion proof terms.
  • Dynamic typing. Collection of types assigned to a term can grow in a process of term building.
  • A free mixture of types from different levels. CL/λ corresponds to a pure level 1 only.
  • Self-referentiality of terms. In LP a type assignment t:F(t) is legal and supported by the standard arithmetical semantics.
  • Internalization as an admissible rule. In CL/λ the Curry-Howard isomorphism relates level 0 (intuitionistic derivations) with the pure level 1 only.

...
Reflexive Combinatory Logic
...

from the slides linked above.

My apologies for the lengthy excerpting; I don't understand the material well enough to summarize effectively. I certainly intend to keep an eye on these developments.

Update: a more comprehensive set of slides seems to be attached to a course on Proof Polynomials that was part of the 9th Estonian Winter School in Computer Science.

The logic of black boxes....

It'll be too hard for me to snip-and-comment on Paul's points, so I'll just wing it freeform.

I agree that the likely trend is toward intuitionistic logic approaches. For example, the logic of "semidecidable propositions" (goes by several other names, and is associated with Abramsky, Hyland, Vickers, and several others). In these systems, one cannot prove a lot of things, only falsify them (by a counterexample). The classic case is of a black box emitting a stream of digits which look a lot like the digits of pi. One cannot prove that the box actually _is_ emitting the digits of pi (that is, that it will do to the end of time), only disprove that it is, by finding a case where it fails to emit what one knows (by other means) is some correct digit of pi.

This approach has much actual practical application: many systems behave as black boxes, at least to those other than the designers (the "God's eye view" that can look inside the box, and maybe prove things that external observers cannot--and even here, in something I hope to get to, there may be surprises, as in "But the laundry chute function was intended to accept bags of laundry as input and output them at the exit point...it was not intended to let prisoners escape!"....an example of "opportunistic typing," perhaps.

Systems of very real everyday importance which act as black boxes to many observers are financial systems (which can be gamed, broken, undermined, and which are of unprovable reliability), computers (which can have weird things done to them, such as buffer overruns), role-playing games, ecological systems, prisons (as above), Boeing 777s which may crash unexpectedly, etc.

In a financial system, for example, it is very important for users of the system to look for various ways the system may fail, and these can happen in a *lot* of ways. The random number generator may be flawed, or can be fed with certain numbers. The owners may have certain kinds of access. And so on. (These things have actually killed some digital banking and stock-trading systems. Users discovered "affordances" that allowed them to game the system, even trigger runaway inflation of digital currencies, etc.)

Some of these affordances were not intended by the original designer. (Schroeder calls this "thalience"--cf. Wiki--when systems form new types or categories different from what a designer considered. The connection with Heidegger is clear. A rock may not be typed in some object ontology as a hammer, it may not have "hammer methods" in an explicit sense, but some actor/player who picks up a rock and uses it as hammer in some online game has exploited its "hammerness"--possibly even breaking the intended rules of the game. An animal who crawls into a log for shelter is "opportunistically typing" a function or object for use in a different way. Heidegger calls this making use of "equipment."

This may be a direction for type systems to go, sort of a "super ad hoc polymorphic typing." (Different from static and dynamic typing, as this is more of an _iterated_ learning process, in the same sort of way the iterated prisoner's dilemma is different from a run once implementation.)

The black box (and intuitionistic logic) connection is that more and more of our software systems involve limited information about parts of the system, about legacy code, about other systems, as in networks, and about the goals/intentions/backstory of other players or agents or systems. (It is not surprising that many of these things come to the fore when we imagine _malicious_ opponents, in banks, games, voting systems, denial of service attacks, digital money, and so on. Attempts to break these systems, cheat them, find loopholes, crash 777s, etc. are cases where attackers are seeking to find the rules, find exceptions, and even find affordances (such as where using a particular number opens an account, or where a laundry chute, real or virtual, is an escape path).

Related to this of course is all the work on agents with bounded rationality or resources, game theory issues with bounded resources, and essentially all "big" systems where the God's eye view just plain isn't feasible.

Also related, but in ways I'm less sure about, are capability-based systems (as in E, etc.) and the connections with typing and affordances. (Capabilities are a way to severely constrain access to certain things or places, just as one might give a key only to the garden shed for a caretaker and not the keyring for the entire house, or give read/write access only to limited things in a system....this is to avoid certain affordances, such as the caretaker gaining access to the checkbook or the jewelry.)

Sorry for any scattershot conceptualizing here. They all seem closely related to me. Analyzing systems "in the large" seems to be a very practical topic.

I Always Had Difficulty Grasping "Affordances"...

in the Heidegerrian sense (sorry, couldn't resist). In particular I have seen no clear formal formulation of affordances.

An affordance appears to be, in some sense, the result of a change in point of view. This is not very useful analytically.

As you (Tim May) show in your post below, an item from one man's ontology can be the source of another man's (e.g., the malicious opponent's) affordance. I know how to formally express the ontology but not how to formally express an associated affordance, other than to say "It's something not in the ontology that, when added, causes no contradictions in the ontology". So in logical terms, an affordance would be a set of additional axioms to be added to our ontology's existing set of axioms. Unfortunately also the possible sets of additional axioms appear infinite.

But I don't see how that is more useful, since now we're back in logic and we're faced with the same old frame problem as before which IIRC was one of the reasons for bringing up Heideggerian affordances in the first place.

Does anyone know of any formal mathematical or logical expression of Heideggerian affordances?

numerical methods

...I think good programmers need more of this kind of mathematics than they do of calculus or numeric methods.

I heartily agree. Too often the fine points of mathematical thinking are lost in calculus and numerics classes. I remember real and complex calculus as a tangled hair ball of rules of thumb, abuses of notation and, of course, rote memorization. Somehow, I never managed to learn how the reals relate to the rationals...only years later am I patching in all the holes. (Actually, I just forgot everything -- I let that old building fall down, and now must build a new one!)

It's a real tragedy that calculus is required in disciplines where it's little used in comparison to the more fundamental skill of reasoning about relations. An emphasis on mathematical thinking, as opposed to mathematical techniques, would benefit not only our profession, but also the social sciences and business and economics, whose students are usually given a brief dip in stats and calc, with no effect on their general reasoning ability.

Math for programmers

I heartily agree with your hearty agreement!

When we look at the kinds of mathematical thinking that most programming projects require, it's not usually (at least not now) about numerical recipes, array manipulation, finding roots. Sure, this was important in the 50s and even into the 70s, and is still important for graphics (splines, ray-tracing, etc.). Or bioinformatics (strings, alignment, etc.). But programmers doing these kinds of things are a small fraction of the total (and they are often first and foremost specialists in their respective areas, only programming to do specific kinds of orbital calculations, industrial processes, CAD, BLAST stuff in bioinformatics, etc.).

The argument I used to hear was that exposure to calculus and linear algebra would also teach basic reasoning. Ha. While linear algebra is really, really cool, and provides concepts that one ought to have (vectors, transforms, the base of a space, eigenvectors and fixed points in mappings), a lot of students never get exposed to conceptual stuff once they get to college.

I learned more logic and set theory in high school, from a great geometry teacher, than I did in my physics-oriented math classes later on. However, I also took some "analysis" classes which focussed on point set topology and gave me a lot to think about and use later on. Reading how point set topology can be implemented in Haskell, with properties of compactness, convergence, open sets, and even Tychonoff's Theorem having direct parallels (functorially speaking!) is just plain mind-blowing. (Cf. the long monograph by Martin Escardo, http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf )

I would love to see the undergraduate curriculum offer a class with coverage of these kinds of issues. For the mathematically sophisticated, they could jump right in on the issues above. For those with less mathematical sophistication, an introductory class covering set theory, Venn diagrams (*), different kinds of logic (including sequent logic), modal logic, the structure of the real line, what proof means, and so on. A later class, perhaps in the 3rd quarter (or late in the second semester) could touch on category theory, functional programming, and logic programming.

Alas, if the main debate in CS education seems to be about dropping the use of Scheme or similar languages and getting students doing Java or C their freshman year, then clearly the chances of teaching them some abstract math are nil. And C is not nil.

--Tim May

The Beseme Project

You might be interested in taking a look at the Beseme Project, assuming you haven't already seen it. The idea behind the project is to develop the kind of undergraduate curriculum you say you'd love to see. Indeed, quoting from the project description:

The Beseme Project (three syllables, all rhyming with "eh") seeks to support education in the application of mathematical reasoning to software development and to provide evidence that experience with these concepts makes software engineers more effective.
The basic syllabus for their core course covers propositional and predicate logic, basic set theory, recursion, induction, invariants, relations, and functions. Many of the exercises are apparently carried out using Haskell. The project makes the course materials are available to instructors at other colleges. They don't (yet) seem to include any category theory, from what I can tell. But perhaps they'll develop a more advanced course to cover that ground (at present the advanced courses seem to be more applied, e.g. used of the ACL2 proof assistant to engineer software). The Math-In-CS.org website also has a few interesting links.

Beseme...I hadn't heard of

Beseme...I hadn't heard of it, but the proposed curriculum looks just about exactly what I think would be good. The principal investigator, Rex Page, I remember from various papers and even some ancient BASIC and FORTRAN books from the 70s (including "WATFIV For Humans"--I absolutely despised FORTRAN IV with WATFIV, but this could've had a lot to do with using an IBM 360/75 in 1971! I had no idea computers were even interesting until a few years later, when I joined Intel. (And Rex Page has been doing more FP kinds of stuff in recent years.)

Looks like the Beseme Project basically ran from 2000-2003. It may still exist, but, like a lot of funded programs, the focus of the people moves on to other things. I see that of the students is in Oregon, completing her Ph.D.; and she worked with Mark Jones on the Programmatica project.

Anyone out there teaching with the Beseme materials?

Beseme was discussed here

Beseme was discussed here several times, so searching the archives may prove useful.

"So, I guess I need to

"So, I guess I need to figure out if category theory, compared to a higher-order predicate logic, would make both a better programming language and a better database model."

I'm not sure what you mean by these comments. My bias, for several years now, has been for FP over logic programming, for Haskell over Prolog (or Mercury). But the reasons are not because category theory is somehow better than what you mention.

And I'm really unsure how you picture category theory being applied to database design. (Although I recall an effort in the late 80s, early 90s, by Henson Graves, called "Algos," which attempted to use category theory for a data base program of interest to the CIA. A friend of mine worked for them at the time, and this was when I first learned something about category theory. Last I Googled him, Graves was a defense contractor, not working directly on Algos, insofar as I could tell. There are some interesting possibilities, but this is pretty researchy. And I also read someplace that when even when some of the pioneers of "cylindric algebras," notably Tarski and his students, were told that relational databases could be seen as a kind of cylindric algebra, they were skeptical....finding the connection was hard even for them, and was certainly not something Codd was thinking of when he did the early work on relational databases!)

It's probably best to view category theory as something to know a little bit of, to appreciate the basic concepts, and to provide a firmer foundation for thinking about processes, change, "commutative diagrams," and functional programming.

A really nice and very deep book is Paul Taylor's "Practical Foundations of Mathematics," which is very theory-oriented, despite the title. He ties a lot of these topics together, especially in the opening chapters (later chapters are pretty rough going, I find).

Philip Wadler has put out several papers on the deep connection between logic and programming, such as "From Frege to Gosling" and variants. I recommend these. And Wadler is of course no stranger to category theory, having "mined" one of Moggi's results about monads and computation for the implementation of monads in Haskell. (Wadler makes a great point in a audio interview he did for "Dr. Dobbs's Journal" that stealing or mining ideas from mathematics can often be very fruitful.)

So while I would not get into any kind of advocacy campaign and say that category theory is more important that predicate logic or logic of any other form, I _will_ say that most people I talk to have almost no awareness that such a thing as category theory even exists, whereas they all think they know something about logic. So learning some category theory, and especially the point of view it naturally leads to (the focus on process, or becoming, over static objects or sets) is useful.

In a weird way, category theory is almost to set theory what Heraclitus was to Aristotle.

"One never steps in the same river twice." --attributed to Heraclitus

There are some issues in

There are some issues in your original response. I'm not sure what you are reading as most of them are addressed in most introductions.

A quick response is read Barr and Wells' ESSLLI notes. They are explicitly geared to computer scientists and are a pretty good introduction.

I have -never- seen a "mutually recursive" definition of category. Even approaches that try to use category theory as a foundation are no more "mutually recursive" than set theory. Most definitions are informal, but easily translatable to set theory or are set theoretical. Barr and Wells define a category in terms of the (usual) notion of a graph (which they also informally define.) However, here's one completely set-theoretic definition: A (small) category is a set of objects, O, and a set of arrows, A. We have three (set) functions: id : O -> A, src, dst : A -> O, and a partial function o : AxA -> A (compose, written infix). If f,g in A, then f o g is defined whenever src(f) = dst(g) (f and g are said to be composable). Also we require for all a in O, src(id(a)) = dst(id(a)). Finally we have the usual categorical laws (assuming everything is composable that needs to be): for all f,g,h in A, f o (g o h) = (f o g) o h and for all a,b in O, f o id(a) = id(b) o f = f where src(f)=a and dst(f)=b. If you care, this can easily be extended to rigorously make the category of Sets allowable (by this definition it isn't because the class of all sets isn't a set.) Absolutely nothing was said about what the objects and arrows "actually" were. This is another issue with your above post.

Most introductions to category theory go to pains to explicitly point out that arrows are -not- necessarily (structured) functions, though that is an extremely common case. For example, any monoid is equivalent to a category with one object, the arrows are the elements of the monoid, and similarly for groups only now all arrows are (categorical) isomorphisms. Any pre-order (and thus any partial or total or whole order) is a category with at most one arrow between any two objects; you can, if you like, identify arrows with pairs of objects. From any graph we can canonically create a category where the arrows are the edges of the graph. The category of relations has as objects sets, but the arrows are binary relations. None of these examples have arrows naturally being "functions" or "transformations".

Another minor oddity is your focus on categories and morphisms. Mac Lane introduced categories so he could talk about functors, and he introduced functors so he could talk about natural transformations. Natural transformation was the idea he was trying to capture. There are very few notable categorical notions that -aren't- at the level of natural transformations (one of them is the notion of isomorphism.) The core ideas of category theory: representability, adjunction, (co)limits, (co)ends, indexed (co)limits, Kan extensions, Yoneda, (co)continuity, are all expressed using natural transformations.

If all these proportedly wonderful concepts and discoveries made by scientists go over everyone else's heads, then how is anyone going to benefit?

Just because they (currently) go over your head, doesn't mean they go over "everybody else's".

Is it any better than set theory and predicate calculus, as far as abstraction is concerned? If so, how? What kinds of inferrable details does it abstract away (if it were to be employed within a programming language)?

"inferrable"? Usually the details abstracted away are irrelevant not inferable. Usually category theory isn't "employed within a programming language", neither is set theory or predicate calculus. Usually these things are applied -to- programs/languages/programming languages theory (and of course many other things). However, most people find category theory more "abstract" (in the way CS people take the word) than set theory. A(n extremely) simple example is isomorphism: if f : A -> B and g : B -> A then f is an isomorphism (and so is g and making A and B isomorphic) if f o g = id and g o f = id. This simple categorical notion captures the idea of bijection, homeomorphism, all algebraic isomorphisms, logical equivalence and others I can't think of off-hand. It accomplishes this because category theory doesn't care (it abstracts away from) what the arrows are. In programming, an abstract data type is defined by the operations it supports and the laws the satisfy; category theory is similar. Something is a product in category theory if it supports some operations that satisfy some laws regardless of how it's represented (or what "operation" means in the context as long as it's an arrow in a category). And so on and so forth.

Is there a simple real-world metaphor to categories? I wonder how similar category theory is to mainstream-industry OOP.

There's a simple real-world metaphor for predicate calculus or set theory? Finite set theory, yes; what we actually mean by set theory, no. How similar is set theory to mainstream-industry OOP? This question barely makes sense. Category theory is a branch of mathematics, not a programming paradigm.

How is it used to mathmatically/logically model story problems (like the kind you solve in a math class)? Can anyone produce story problems that can elegantly be solved using category theory, or that demonstrate the effectiveness of its paradigm for mathematical/logical modeling?

Again, where do these questions come from? How is set theory or predicate logic used to model "story problems"?

Its most significant practical applications have been towards unifying, organizing and generalizing many existing mathematical concepts. However, there have been several more practical applications. It is intimately related to denotational semantics, coalgebra and coinduction probably wouldn't be nearly as developed as they are now without category theory (and it has myriads of applications: automata, data types, semantics of OO, semantics of concurrency), (O')Caml stands for (Objective) Categorical Abstract Machine Language; it clearly inspires many ideas in actual programming: folds, monads, functors, unfolds; it has a strong relationship to logic and programming, the Curry-Howard correspondence is sometimes referred to as the Curry-Howard-Lawvere or Curry-Howard-Lambek correspondence; the theory of institutions influenced many module languages and was most overtly applied in the OBJ family of languages; proofs in category theory tend to be constructive, if you interpret the proof that the existence of a terminal object, pairs, and equalizers implies all finite limits exist you get exactly the unification algorithm except that this holds in -any- category with those things so you get a whole family of unification algorithms most notably the OBJ family of languages uses this for order-sorted logic (what you get when you specialize unification to the category of partially ordered sets).

Hmm...

I have -never- seen a "mutually recursive" definition of category

...

Absolutely nothing was said about what the objects and arrows "actually" were

Exactly. Obviously, at the time of OP, I hadn't made the intellectual leap, and I was seeing categories defined in terms of objects and arrows, and arrows defined in terms of morphisms: in mental terms, foreign concepts defined in terms of foreign concepts, which sounds like a recursive description to me!

"inferrable"? Usually the details abstracted away are irrelevant

Yes, inferrable, meaning that they can be automated via a compiler or interpreter, but never irrelevant to the machine--only to the domain model.

Usually category theory isn't "employed within a programming language", neither is set theory or predicate calculus

Ah, but what if they were?..(sigh) It wouldn't be too hard to do. I can think of serveral systems that strive for this.

Most introductions to category theory go to pains to explicitly point out that arrows are -not- necessarily (structured) functions

Quote from my OP (emphasis added):

a morphism seems to be a transformation (possibly represented by one or more functions)

Don't forget your modal logic.

Just because they (currently) go over your head, doesn't mean they go over "everybody else's".

You're right--all programmers are computer scientists. I forgot that. Anyways,

Category theory is a branch of mathematics, not a programming paradigm

Who said that has to be strictly true? I'm going to put this on my top 10 funniest quotes of the year. That strikes me as so funny! LOL

Again, where do these questions come from? How is set theory or predicate logic used to model "story problems"?

Well, you go ahead and try doing a proof of contradiction on that one. If you can prove that set theory and predicate calculus can't be used to create logical or mathematical models of a story problem and then be used to solve it, then I will stop wasting my time with them this instant! LOL!

have fun in your box; LOL!

(No hard feelings) :-)

Don't forget your modal logic.

Don't forget your modal logic.

You are very perceptive. I mentioned coalgebra above and it is indeed deeply linked to modal logic. A different set of ESSLLI notes.

Right under my nose all along!..

Has anyone noticed the similarity between those point-arrow diagrams commonly shown in category theory, and state transition diagrams?..

Suddenly, category theory is a little bit easier to understand.

This will definitely help teach category theory to the masses!

. . .

So, I guess I need to figure out if category theory, compared to a higher-order predicate logic, would make both a better programming language and a better database model.

I'm not sure what you mean by these comments. My bias, for several years now, has been for FP over logic programming, for Haskell over Prolog (or Mercury). But the reasons are not because category theory is somehow better than what you mention.

I'm not interested in prolog. It's much too watered down from the original power of predicate logic, which beats prolog hands down. I'm just trying to see if there is any other potentially existable programming language that is better than predicate logic (with set theory et. al. appended), and if so, what is it?

Currently, category theory doesn't look all-encompassing enough: it doesn't seem to distinguish between an object (a type) and a specific instance of an object, which could (though I haven't thought this through) be important for databases and knowledge representation schemes. The obvious alleviation for this would be to append category theory (instead of set theory) to predicate logic. Then, I would be able to have category, functor, and natural-transformation inference, but then I heard somewhere that category theory was an alternative to logic. If so, then how? How can it replace logic? I still have some work to do.

Sounds like you're looking

Sounds like you're looking for n-categories. I'll let someone else fill in an explanation beyond "layering categories on top of each other so that each categories arrows are the objects in the category above it".

Look closely at the definition

Has anyone noticed the similarity between those point-arrow diagrams commonly shown in category theory, and state transition diagrams?

Let S be the set of states of some state machine. Let T be the set of possible (possibly multi-step) transitions. In other words, let T consist of pairs (A,B) where the machine could go possibly go from state A to state B (after some, possibly zero, transitions).

Now look at Wikipedia.

We have a set of states. Call them objects. We have a set of transitions. Call them morphisms. Given any transition, we can extract two states from it, the initial state and the final state. Call the first the source and the second the target.

Keep working through the definition...

If there is a transition from a to b, and a transition from b to c, then there is a transition from a to c. So define (b,c)o(a,b) to be (c,a). Note how if u and v are transitions where the target of u is the source of v, then vou is also a transition. Note that we also have transitions (a,a) for every state a, corresponding to the zero step transition.

I'll leave checking for associativity as an exercise.

The point is, in computer science categories are everywhere. The notion of a category can be adapted to fit many things. The rule is, any time you see a diagram with lots of arrows and the heads of some arrows point to where the tails of arrow emerge there's a chance you have a category lurking there. Just check to see if the axioms fit. And any time they do fit, then any theorem of category theory may be applicable to these diagrams and may tell you something new or useful.

problem 0

I'll leave checking for associativity as an exercise.

(c,d) o ((b,c) o (a,b))  =  (c,d) o (a,c)  =  (a,d)
((c,d) o (b,c)) o (a,b)  =  (b,d) o (a,b)  =  (a,d)

It wasn't much of an exercize -- am I missing something?

It wasn't much of an exercize -- am I missing something?

You're not missing a thing. I'm trying to convey the message that there's nothing weird or circular in the definition of a category and that the various clauses in the definition mesh perfectly with some ordinary everyday intuitions.

State transition systems

I'm not saying you're doing this, but I want to suggest some care in identifying categories and state transition systems. A typical way of formalizing a state transition system is to use an M-set where M is some monoid. In the descriptions above the category is being used in place of the monoid, not the whole M-set. This is indeed natural as a category can be viewed as a generalization of a monoid (a monoid is a one-object category). This suggests talking about C-sets where C is some category and indeed this is exactly what Barr and Wells do in the lecture notes I referenced above. If you go with this, it turns out that the various pieces correspond to very non-specialized ideas including a perspective on the Yoneda functor.

I don't know if this is a "practical application," but...

...A Solution for the POPLmark Challenge:

We present a partial solution to the POPLmark Challenge [1] based on Nested Datatypes in the Coq proof assistant. Our formalization addresses part (1A) of the Challenge. This work is a radical improvement of our previous attempt... This formalization is part of our effort to put Modules over Monads and Nested Datatypes at work for reasoning about languages with bindings. The theory supporting our vision is exposed in Modules over Monads and Linearity... This new version is about 5-6 times smaller than our previous attempt published in may 2006.

Modules

A quick glance at this paper shows that the authors rediscovered (in a very special case) the old concept of (bi)modules introduced by J. Benabou:

Let S : A -> A , T : B -> B be two monads in a bicategory W. The composition with S and T gives rise to a (standard) monad on Hom(A, B). A module from S to T is an object in the Elienberg-Moore category for this monad.

Best,
MRP