|
Using category theory to help write programs is a cool idea, but
when I was reading the paper I was continually muttering to myself ...ok now
show me some code...some CAML code or Haskell or Scheme code....
show me how to write a program with category theory!
(Note: You can supposedly do this in the language "Charity" which I will
probably never have the time to learn.)
Code would give me a concrete anchor that I could work backwards from
to see how in fact category theory could help me write programs,
but alas it doesn't happen, I'm stuck with a spec that maybe I feed
into some proprietary code generator.
To quote the paper:
>It is unlikely that a general automated method exists for constructing rungs of the
>ladder, since it is here that creative decisions can be made......
>Our goal in Designware is to build an
>interface providing the user with various general automated operations and libraries of
>standard components. The user applies various operators with the goal of filling out
>partial morphisms and specifications until the rung is complete.
Sounds roughly similar to what Alexandrescu is doing with his implementation
of design patterns with C++ metaprogramming in
"Modern C++ Design: Generic Programming and Design Patterns".
except C++ and GOF are radically popular and category theory is traditionally
an abstruse and unapplied branch of mathemetics and Alexandrescu actually does
implement design patterns directly in C++ (immediate gratification):
Quoting Hoare [6]: "Category theory is quite the most general and abstract branch of
pure mathematics. The corollary of a high degree of generality and abstraction
is that the theory gives almost no assistance in solving the more specific problems
within any of the subdisciplines to which it applies. It is a tool for the generalist, of
little benefit to the practitioner."
Hence it will come as no surprise that, for algorithmics too, category is mainly useful
for theory development; hardly for individual program derivation.
(From: A Gentle Introduction to Category Theory
Maarten M. Fokkinga, available online)
(Quoting: C.A.R. Hoare. Notes on an Approach to Category Theory for Computer Scientists. In
M. Broy, editor, Constructive Methods in Computing Science, pages 245{305. Interna-
tional Summer School directed by F.L. Bauer [et al.], Springer Verlag, 1989. NATO
Advanced Science Institute Series (Series F: Computer and System Sciences Vol. 55).)
-------------------------------------------------------------------------
Possibly Ridiculous Over-Generalization:
Category theory is to functional programming what
'refactoring' is to object oriented programming?
Categories make functional programs more understandable
via mathematical refinement?
"Refactoring" through a refinement of programming style towards
readability (kind of like a "Strunk and White" for programming)?
One difference seems to be that "refactoring" codifies existing programming practice
with easy to follow rules of thumb and works directly with code.
It's not attached to specific black-box proprietary systems like
"Specware, Designware, and Planware."
-------------------------------------------------------------------------
It seems like:
The success of Alexandrescu's methods stems from taking
ideas from the Lisp world that were stillborn in the AI winter of the
early nineties, namely object oriented meta-programming and
the meta-object protocol (MOP), grafting it onto the C++
(that since the introduction of templates has been sitting there ready for it)
and doing something useful with it: implementing design patterns.
Truly "meta" : C++ templates under Alexandrescu's Loki Design Pattern Library
under whatever functionality you're implementing with the design pattern
(e.g. directory walking, code generation....)
Now if there was a CAML or Oz category theory library and I could use it for
meta-programming....let's say stateful folds (catamorphisms) for walking
directory trees or XML queries and transformations, but my imagination
is running away with me and grey matter + patience = mathematician,
both of which I lack....
| 
Mechanizing the Development of Software