On 7/13/07, William Sit <[EMAIL PROTECTED]> wrote:
.. Whatever the primitive types are, the important thing is that there be a well-designed user interface (exported functions) on par with all other algebra code. Right now, Tuple and Union are "inaccessible" from the algebra layer without going to lisp (Record seems okay ). That is, in my view, a design flaw. They should be designed as if they were genuine domains (where one can construct elements and extract information from elements and compute with them). How they are implemented and optimized at the lower levels should not be of concern to the algebra layer.
+1 Yes, exactly! There should be no need ever to "escape" to lower levels. Already Axiom and Aldor use different internal representations for many things including Record. But that should be no concern to the Axiom library programmer and in fact for the most part that is accomplished by the magic of the Axiom Aldor interface. But the existing Axiom library code written in Spad has many places where assumptions (often unstated hidden assumptions) about internal representations are made. This ultimately will make modular conversion of the Axiom library to Aldor much more difficult than it should be. But choosing the correct "primitive types" is a rather hard problem. That is in my opinion one place where category theory comes in. We know from very general considerations (topos theory) that if we expect to be able to implement a large part of mathematics (e.g.that part that presumes set theory) in our language we will need a language that is complete enough to at least represent all limits and co-limits plus exponentiation and sub-object classifiers. Category theory contains a theorem that this is possible if we implement just two limits (equalizers and products) and two co-limits (co-equalizers and co-products). It also says that there is a certain kind of redundancy between the combination of limits, co-limits and exponentiation so that it is possible (but quite complicated) to implement co-limits in terms of limits and exponentiation. And vice versa, limits in terms of co-limits and exponentiation. See for example the very quick introductory article by John Baez: http://www.math.ucr.edu/home/baez/topos.html Topos Theory in a Nutshell John Baez April 12, 2006 It turns out that most modern languages already have products (Records) and some form of exponentiation (representation of higher-order functions) but there is considerable variation in the representation of co-products (if they exist explicitly at all). In fact most programming languages have a strong bias away from all notions related to co-limits. However category theory says *exactly* what co-products should be like by the fundamental properties of categorical duality: If we represent the axiomatic algebraic properties of limits in terms of a commutative diagram, then we can obtain the algebraic properties of co-limits simply by reversing the direction of all of the arrows in the diagram. This simple duality has enormous implications for the actual implementation of the primitive types and sometimes quite unexpected consequences. This starts at a very basic level of only looking at a function as a mapping in one direction: f: X -> Y But in any sufficiently complicated category (e.g. Set) arrows come with a "built-in" dual concept f: Y <- X that can be represented in terms of "fibers", i.e. as the family of subsets of X indexed by Y f' : Y -> 2^X http://en.wikipedia.org/wiki/Image_(mathematics) This bias against these dual notions runs very deep and effects the expressiveness of our mathematical programming language in important concepts such as equivalence classes and equality as well as many fundamental ideas that arise in algebraic topology. Which again emphasizes the role of category theory and the need to "get it right" in the choice of primitive types. Further ref: http://en.wikipedia.org/wiki/Topos_theory Regards, Bill Page. _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer