Re: [Axiom-developer] Unions in Spad

[Bill Page]

On 7/13/07, William Sit <address@hidden> 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.