arrow-structure syntax

Francois-Rene Rideau fare@tunes.org
Sat, 5 Dec 1998 00:23:20 +0100


Just some *general* remark about Brian's arrow universes,
independent from the content:
when you know so many arrows, I expect that you know category theory,
which is the theory of arrows par excellence.
I was originally invented for algebraic/geometric used,
but it has been since used to independently reconstruct type theory
as known in typed lambda-calculi...

I don't know category theory *that* well, but enough of it to know that
* it's very powerful
* it's mostly the same as lambda-calculus,
 only with a graphical rather than syntactical formalism.

What I mean is: there are lots of things that we don't have to reinvent,
and that we shouldn't reinvent, because it's already there.
I certainly do not mean to lessen any one's talent.
But I'd rather learn known things from a book, and discover new things,
than discover known things the hard way, and have no time for new things.

## Faré | VN: Уng-Vû Bân   | Join the TUNES project!  http://www.tunes.org/ ##
## FR: François-René Rideau |    TUNES is a Useful, Not Expedient System     ##
## Reflection&Cybernethics  | Project for a Free Reflective Computing System ##
Living on Earth may be expensive, but it includes an annual free trip
around the Sun.