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

[William Sit]

Gabriel Dos Reis wrote:

> On Sun, 12 Aug 2007, William Sit wrote:
>
> | Isn't the problem whether 'Monad has SetCategory with "*":(%,%)->%' ?
>
> If the question is formulated in terms of "has", then I think the answer
> is unambiguously "yes".
>
> But, is that the way the compiler is intended or does the matching of
> actual arguments with formal parameters?
>
> It seems to me that the compiler asks the question in terms of coercible,
> instead of "has".
>
> -- Gaby

I believe for category parameters, the compiler checks whether the supplied 
domain
"has" the category, and for domain parameters, the compiler checks whether the
object belongs to the domain, NOT whether the object is "coercible" to it. I 
believe
coercion is not always automatic in Spad (but is in the interpreter, even when a
domain does not explicitly have CoercibleTo the target --- see examples in
http://wiki.axiom-developer.org/SandBoxCategories).
The Spad programmer has to explicitly call a coerce function (and if that does 
not
exist, define the domain to be CoercibleTo the target domain and define and call
coerce) before passing the object to the routine or constructor.

Matching of actual arguments with formal parameters does not mean "is" but means
"belongs to". In this sense, if the formal parameter is a category (or a Join of
categories), the actual parameter need to be a domain in that category (or all 
of
the categories listed in Join); if the formal parameter is a domain, the actual
parameter need to be an object in that domain.  The question of category 
equivalence
comes in only when the two formal arguments have the same defined structures. 
Then
the question of whether a domain "belongs" to the categories specified depends 
on
how the domain is constructed. If the formal argument is named, then the domain 
must
be explicitly declared to belong to that named category to be a valid argument. 
If
the formal argument is unnamed, or rather, has unnamed components (in the sense 
that
'SetCategory with ...' is 'Join(SetCategory, with ...)', where 'SetCategory' is
named, and 'with ...' is unnamed), then the unnamed category may be satisfied 
if the
domain structurally belongs to the unamed category (there need not be, and 
cannot
be, an explicit declaration, except in the sense of exported functions).

Similarly, the question of domain equivalence comes in only when two formal
arugments have the same defined structures. Then the question of whether an 
object
"belongs" to the domain specified depends on whether the formal argument is 
named or
not. If named, the object must have been declared to be (and assigned a value 
from)
the said formal domain argument. If unnamed, the object must also have been 
declared
to be (and assigned a value from) the said formal domain argument. Actually, I 
am
not sure if there is such a thing as an unnamed domain. In Davenport's example, 
to
me,  'List Integer' is certainly a named domain from domain constructor List. Of
course, if you declare t:SetCategory == List Integer, or t:= List Integer, then 
you
have renamed the domain and t would not be the same domain as List Integer for 
the
purpose of compiling Spad. Again, see

http://wiki.axiom-developer.org/SandBoxCategories

for examples.

William