The state of the art for Arrow specs

[Brian Rice]

Well, I've been working through all sort of ideas for implementing basic
Arrow functionality, and have worked out a lot of the ideas, though some
areas remain open.  What remains is not impossible to implement, but I am
insisting on a clean design so that the system's model of itself will be
simple.

So, here are some of the "primitive" arrow objects:
(1,2) "car" and "cdr" (or "head" and "tail" or whatever): these are two
graphs which contain all off the reified references that all arrows in the
system contain.  Note that this is a recursive definition, since arrows in
"car" and "cdr" can have their references reified as well.  This allows
arbitrary reification of references.

	The axiom amounts to:
	for each arrow X, there is an arrow in "car" whose car is X and whose cdr
is the arrow referred to by X's car slot, and there is an arrow in "cdr"
with the corresponding definition.

	Note: Reifying a reference has nothing to do with obtaining the arrow
referred to.  More on that below.

(3) Treating a graph as a function and applying it to an arrow.  This
amounts to an "apply" graph which contains the arrow referred to by all
arrows' cdrs.  (Visualizing this is left as an exercise for the masochist.)
 Inverting a graph's arrows allows one to invert the function obtained.  As
far as seems obvious, this service would be invoked by drawing arrows
between the argument and the function, but the complete system's picture
will probably be much more interesting.

	The axiom amounts to:
	for each arrow X and graph G, return all arrows Y for which there is an
arrow in G whose car is X and whose cdr is Y.

	Note: In combination with the car and cdr graphs, this can be used to
obtain the arrows referred to by a given arrow indirectly, which is what
programming is all about.
	Note2: If the graph as a function is multiply-defined, this could be used
as a concurrency mechanism or as quantification over a set of values, like
a type.  This could be highly-useful in any case.

Now, obviously these tools allow us to obtain the arrows that argument
arrows actually refer to.  However, this says nothing overtly about how to
obtain arrows that refer to the target arrow, which means that
meta-information is so far inaccessible.

(...) Now, what remains is the system for specifying graphs, which seems to
me to naturally be a system for taking certain graph constructs and
modifying them incrementally using cleanly-defined arrow functions to
produce graphs of all sorts.

Also, the appropriate analogue of quantification is still missing, although
a simple solution seems to be to predicate a graph that specifies a type,
and infering from an arrow's membership in the graph that other statements
apply to it, a la formal logic.  The problem there is that one runs into
the problems of set theory, which might be very complex for Arrow.
Alternatively, our "function" above could be applied to the meta-graph of
the set, returning all the elements (in an abstract sense) and performing
evaluations based on the properties of those arrows.

I will post updates to this spec incrementally.

Comments are, of course, highly welcome.
	-Brian