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

[Bill Page]

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.