categories: RE: Question

[S.J.Vickers@open.ac.uk]

Dusko says:
> it's interesting that almost no one took michael healy's bait (attached).
> 

Here's a message I sent to Michael Healey privately:

>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
There's a minefield of hotly held opinions behind this question, but let me
try to give a couple of pragmatic considerations.

1. What is the most appropriate characterization (for present purposes) of
collections? By elements or by functions? Set theory postulates that a
collection is entirely determined by its elements. If functions are better,
that's beginning to look more like a categorical approach.

Examples:
Topology - a space is not fully defined by saying what its points are. You
only capture continuity when you look at the maps between spaces.

Type theory - syntactic terms in general have free variables in them,
effectively parameters, and these really correspond to functions rather than
simple elements.

2. Do you want to consider a variety of logics? Set theory as such is
solidly classical. To relax that you need to consider different formal
systems, and then category theory usually provides tools for achieving
better presentation independence than more syntactic approaches.
<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<

In this hurried response to Michael's posting I was trying to get across
some sense of how category theory can help you see the wood for the trees -
the "better presentation independence" is what Dusko refers to as
"structuralist maths".

> for software engineers, foundations are the link with the meaning of their
> programs. having a slightly shorter history than math, they do not have
> languages as natural as arithmetic, or calculus, but have to chose between
> KIF and Ontolingua, and the various other versions of esperanto every day.
> categories dam the flood of structure in software engineering, just like
> they originally did in homology theory almost 60 years ago. some good math
> may come out of it if taken from a good side.

I agree.

I looked up keywords like SUO (Standard Upper Ontology) and KIF (Knowledge
Interchange Format) - they are about standard notations for expressing
information - and some key issues seemed to be rather basic things like the
meaning of first order logic.

I found this depressing. As we know, categorical logic has some very clear
accounts of this that have the great virtue of bringing out deep structure
over superficialities of the logical syntax. It also makes it easier to
question whether "self-evident" notation and axioms are actually meaningful
and valid.

But how can we bring these insights to the software engineering masses? It's
not enough to say "first learn about category theory and then look for
adjunctions, monads and <favourite keyword> everywhere". With this approach
it seems all too easy to prescribe people categorical logic as a cure for
their myopia, and then to find them trying to use it as reading glasses and
wondering why it doesn't work.

One of the things that makes Mac Lane's book such a masterpiece is the way
it uncovers category theory as something already understood rather than
presenting it as something new. The working mathematician is well familiar
with reasoning about adjunctions and monads in special cases, and it's
"just" a matter of uncovering the underlying pattern.

Speaking for myself, after all these years I still understand a lot of
category theory not in the abstract but through paradigms. Enriched
categories? They're just rings, really. Or, at least, ringoids. Presheaves?
They're just modules. Yoneda embedding? The free module on one generator is
just the ring itself.

The software engineer does not have the working mathematician's body of
knowledge. I think to give them category theory we first have to explain,
without mentioning categories, just why structure has to reside not inside
the objects but amongst the morphisms: to explain a collection by its
elements alone is not enough, even in a very basic logical framework.

Steve Vickers
Department of Pure Maths
Faculty of Maths and Computing
The Open University
-----------
Tel: 01908-653144
Fax: 01908-652140
Web: http://mcs.open.ac.uk/sjv22