Re: [Axiom-developer] "has" and "with" (was curious algebra failure)

[William Sit]

I think I understand the objection raised by Gaby. In matching Monad to
SetCategory with ..., Axiom is applying a forgetful functor that, given a
monad, forgets all of its operations except those featured in SetCategory with
....   In this sense, applying a forgetful functor is a form of automatic
coercion on the level of categories.  Gaby is correct in saying that strictly
speaking, the forgetful functor should also not be automatic, just like the
usual coercion between domains. In fact, how one forgets the structure of a
ring to the structure of a Monad would be ambiguous, since there are two
possible ways. For more complicated algebraic structures (like Hopf algebra,
differential algebra) if it is possible to specify precisely the forgetful
functor, it would allow us to have only one Monoid structure instead of an
AbelianMonoid and a Monoid (and many others distinguished by different names
for the monoid operation).

Gaby, is that a fair statement?

You may be interested in this old 1986 article by Kamal Abdali et al., on An
Object Oriented Approach to Algebra System Design:

http://portal.acm.org/ft_gateway.cfm?id=32444&type=pdf&coll=GUIDE&dl=ACM

One of the stated features of Views is:

"Views do not depend on operation names. That is, locally (i.e. in their
domains) two different Rings may have different names for their 'additon
operation', but, when viewed as Rings, their addition operation is accessed by
the same identifier."

To allow for such a goal, the compiler will have to be redesigned, as well as
most of the algebra code.


William

Bill Page wrote:

> Gaby,
>
> On 13 Aug 2007 00:28:49 -0500, you wrote:
> > "Bill Page" <address@hidden> writes:
> >
> > [...]
> >
> > | > > I'm saying that the parameter S of the default package
> > | > > Monad& -- generated for the default implementation of the
> > | > > category Monad -- is of the named category Monad.  It is
> > | > > that parameter S which is being used to instantiate
> > | > >RepeatedSquaring.  However, RepeatedSquaring expects its
> > | > >(domain) argument to be of the unnamed category
> > | > >
> > | > >    SetCategory with "*": (%,%) -> %
> > |
> > | Your statement of the problem is a little confusing to me since the
> > | parameter S is the parameter of RepeatedSquaring. But as you say, it's
> > | type is given by the unnamed category above. You are concerned because
> > | what is being passed to RepeatedSquaring is a domain of type category
> > | named Monad. But clearly a domain of type Monad is also is a member of
> > |
> > |    SetCategory with "*": (%,%) -> %
> > |
> > | since Monad is a subcategory of this category - any domain that "has"
> > | Monad will necessarily provide all of the exports required by
> > | RepeatedSquaring. RepeatedSquaring requires it's (domain) argument to
> > | be of type that is a subcategory of this unnamed category.
> >
> > Bill, it is getting late so I'll try to give a longer reply later.
> > I just wanted to say one thing:  We should distinguish the notion of
> > "being of a member of T" from "being coercible to T" -- as the Spad
> > language does.  Argument passing in function calls follows the
> > semantics of  "being coercible to the type of formal parameter".
> >
>
> I was trying to use the terminology in Section 12.5 Membership, of the
> Axiom book on category hierarchies and also section 7.6 Type
> Conversion, of the Aldor User Guide on the sub-type relation. In
> general coercion (or conversion) is used to mean something a little
> more "mathematical" in Axiom. In fact 'CoercibleTo' is a category
> constructor in Axiom.  For example one might say that Integer is
> coercible to Float but that is not the kind of conversion
> automatically considered by the Spad compiler.
>
> I look forward to reading your longer reply.
>
> In Spad there is also the subdomain construction that is used to
> define PositiveInteger and NonNegativeInteger from Integer. Subdomain
> automatically provides "coercible to" the parent domain. This is
> something that Spad has that was never implemented in Aldor. We had
> some discussions about this a few year ago on this list. I was not
> convinced that the concept of subdomain is a dispensible part of the
> Spad language - even though it is not currently widely used in the
> Axiom library code. I general I want subdomains (and sub-object
> classifiers) for the same reason as I want records (products) and
> unions (co-products), because this is a step toward a more categorical
> semantics for the language.
>
> Regards,
> Bill Page.
>
> Regards,
> Bill Page.
>
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> http://lists.nongnu.org/mailman/listinfo/axiom-developer

--
William Sit
Department of Mathematics..Email: address@hidden
City College of New York................Tel: 212-650-5179
New York, NY 10031, USA.................Fax: 212-862-0004
Home page: .......http://scisun.sci.ccny.cuny.edu/~wyscc/