Saul Youssef was at least in part, experimenting with the idea that the Axiom library (or rather Aldor libraries) as a whole could in principle be written to be "correct by design" with all domains and categories defined from the ground up as fully categorical constructions.
I like that. But read http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf (BTW, this looks like an example of Literate Programming.) Saul claims that (with a bit of imagination) a object of type Category, i.e. a category in the sense of the Aldor programming language, is a category in the ordinary mathematical sense.
But... Aldor is not enforcing this. One has to build on conventions. I guess it requires a lot of discipline to actually build such a library. I'm all in favour to carry out a (compilable) library in this way. It would probably show in which way Aldor/SPAD can/should be improved to make them really categorical (and still efficient).
The bad thing is that if you require a user of a programming language to know about category theory, you basically say that the language will fail. Well, maybe not if there are enough mathematicians how become interested in programming then. ;-)
Ralf -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
