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.