MOX

[Francois-Rene Rideau]

On Fri, Jan 18, 2002 at 08:54:19PM -0500, Brian P Templeton wrote:
> MOX could implement Arc's
> ``name-munging'' (I have no idea what the real name of the ``feature''
> is) cleanly. (In Arc,
>     (eqcar x y) === (eq (car x) y)
> but in MOX, something like
>     (|eq||car| |x| |y|) === (|eq| (|car| |x|) (|car| |y|))
> with `|...|' denoting an arrow to the object whose canonical name is
> `...', could be cleanly implemented, I think.)

This looks quite like what happens in category theory when you apply
functors, whose effects operate not only on objects, but also on arrows.
The downside is that so as to identify precisely which functor is applied
in which way, you either need a lot of small categorical combinators
everywhere (you know, like, some mapping here, some canonical injection
there), and/or you need some elaborate kind/type system so as to
automatically deduce all those implicit combinators.

All in all, TANSTAAFL: either
the system doesn't try to double-guess the programmer, and then
specifying things precisely can get pretty boring and "low-level",
or you do try to automatically deduce extra implicit information
from what the programmer explicitly provides, and this can only be done
by having a good model of what that extra information is
based on what correct programs are expected,
as opposed to programs that are considered incorrect
(which amounts to an elaborate inferred type system),
which involves extra coding both from the system implementer
who has implement the model, and from the occasional programmers
who'd like to do things not directly expressible in the model.

The programming languages that currently draw most from the categorical
framework seems to be Haskell (does anyone here understand the higher stuff
like catamorphisms, anamorphisms and zygomorphisms in
"The Evolution of a Haskell Programmer"? -- I forgot the URL,
but Google knows it, and so does lambda.weblogs.com).
Other systems based on strongly typed lambda-calculi can also be used
in similar ways (Cayenne, SML, OCAML come to mind,
Coq too though not a programming language).

Maude is linked to category theory in a very different way:
basically, rewrite systems can be seen as particular categories,
and lots of categorical concepts then apply easily --
I chose this formalism to talk about computing systems in my thesis,
for it fits the purpose of reflective systems in a great way.

[ François-René ÐVB Rideau | Reflection&Cybernethics | http://fare.tunes.org ]
[  TUNES project for a Free Reflective Computing System  | http://tunes.org  ]
``why'' is always relative to a model of possible explanations. It is never
an "absolute" question. Which is precisely what makes it meaningful. -- Faré