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

[Bill Page]

Gaby,

On 8/12/07, you wrote:
> On Sun, 12 Aug 2007, William Sit wrote:
>
> | Isn't the problem whether 'Monad has SetCategory with
> | "*":(%,%)->%' ? My answer would be yes. This should not be
> | related to equivalence of categories or domains. We
> | already have seen examples that Integer has with
> | _*:(Integer, Integer)->Integer. Here, we are not saying
> | 'Monad is SetCategory with "*":(%,%)->%'.
>

Sorry for my confusion. In fact I agree with William. This is not
directly related to type equivalence. We need something more general
than type equivalence. We need to know when one category is a
subcategory of another. The type equivalence rules to which Juergen
referred must be applied to the parts of the category expressions in
order to determine this relationship.

You wrote:

> > 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.

In other words the compiler must check that Monad is a subcategory of
the type of parameter S. To do this it can observe that:

   Monad has SetCategory

(this requires rule 1) and that

 Monad has with "*": (%,%) -> %

(this requires rule 2). Originally I thought you were mostly concerned
about these anonymous parts of the category.

> 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?
>

Of course the compiler must be able to check type correctness at
compile-time while "has" is evaluated at run-time but they are closely
related.

When you call a function like

  f:Integer->Integer

you must pass it a member (object) of the domain Integer. Objects are
members of only one domain.

When you call a package, e.g. RepeatedSquaring you just pass it a
member (domain) of the category

  SetCategory with "*": (%,%) -> %

Unlike objects, domains can be members of many different categories
but certainly any domain that is a member of Monad will also be a
member of this category.

The type of a domain is the smallest category that contains all the
categories of which this domain is a member. Equivalently, a domain of
type category X is a member of all the subcategories of X.

> It seems to me that the compiler asks the question in terms of coercible,
> instead of "has".
>

Perhaps by "coercible" what you mean is just forgetting the extra
structure of the subcategory - just like PositiveInteger is a
subdomain of Integer and coercion of a PostiveInteger to Integer is
"natural" because there is a function which injects every
PositiveInteger into Integer. In the Axiom interpreter was can call
the function +$Integer with an object of type PositiveInteger because
such a coercion exists and the interpreter invokes it automatically.

Similarly is might be possible to say that we can call
RepeatedSquaring with a domain of type Monad because there is a
"coercion" (a forgetful functor) that can inject domains of type Monad
into domains of category

  SetCategory with "*": (%,%) -> %

In fact we can do that simply by striking out those parts of the
category expression for Monad that are not equivalent to any
corresponding part of the above unnamed category. If what we have left
is identical to this category, then we know monad is such a
subcategory.

I guess that is the kind of coercion that is being referred to in the
error message you quoted in your first email in this thread:

>> Apparent user error:
  Cannot coerce S
     of mode (Monad)
     to mode (Join (SetCategory) (CATEGORY domain (SIGNATURE * ($ $ $))))

------

It seems to me that the mode we should expect here is not Monad but
rather it's category-value in which case the coercion is obvious.

Regards,
Bill Page