Re: [Axiom-developer] A curious algebra failure

[Bill Page]

On 8/11/07, Gabriel Dos Reis wrote:
> On Sat, 11 Aug 2007, Stephen Wilson wrote:
>
> | Gabriel Dos Reis <address@hidden> writes:
> |
> | > On Sat, 11 Aug 2007, Stephen Wilson wrote:
> | >
> | > | Gabriel Dos Reis <address@hidden> writes:
> | > | > | Here, % certainly satisfies the conditions on the parameter type:
> | > | > |
> | > | > |    SetCategory with "*": (%,%)->%
> | > | >
> | > | > I don't think it does, in the sense of Spad.
> | > | > I believe two unnamed categories define distinct categories 
> irrespective of
> | > | > their bodies.
> | > |

No, that is *not* correct. Unnamed categories are just values of type
Category. They are distinct only if the values are distinct. 'with' is
used to form a category-valued expression.

> | > | Are you saying that % is unnamed?
> | >
> | > `%' is not a category; it stands for the current domain.
> | >
> | > I'm saying that the category
> | >
> | >     SetCategory with "*": (%,%)->%
> | >
> | > is unnamed.
> |

That is correct.

> | Right.  What I am saying is that in the type context
> |
> |     S : SetCategory with "*": (%, %) -> %
> |
> | when % denotes MONAD, the category of % (its `principle category' as I
> | called it, since in the general case it is anonymous), satisfies the
> | context.  Certainly MONAD has SetCategory and an export "*": (%, %) ->
> | %.  The nominal/structural typing rules (not that I have tried to
> | define them formally) are just my way of thinking about the issue.
>
> I think I understand what you're saying.  I'm not sure they match Spad typing
> rules.  See the discussions in sections 12.8 and 12.12 of the Axiom book.
> The short version is that
>
>     domains belong to categories by assertions.
>
>
> | If this interpretation does not hold, what kind of expression could
> | possibly satisfy the context S above?
>
> That is the whole problem. :-)
>

This statement in the Axiom book should really say:

  "domains belong to *named* categories by assertions"

This does apply to anonymous categories.

> As you suggested, I suspect it should have been written like
>
>      if S has SetCategory and S has "*"
>

No, I don't think that is what Stephen is saying.

> The trouble is that we don't want to test just for the name "*".  We
> want to test for the signature
>
>           "*":(%, %) -> %
>

That is precisely what is meant by a domain satisfying a category
*value* (a so called "anonymous" category).

> I don't know how to write that in Spad -- Ralf?
>

I think that sometimes the best way to understand Spad is to look
backwards from the definition of Aldor. A much more rigorous and
consistent definition of Aldor concepts is given in the Aldor User
Guide (AUG) and in most cases these concepts map backwards to Spad
exactly as required.

In this case I would strongly recommend that you (re-)read Chapter 7
Types. Specifically take a look at Section 7.5 Subtypes for a
discussion of category-valued expressions versus named categories and
Section 7.7 Type Satisfaction. Also most of section 7.9 Categories
especially to understand the use of 'define' to refer to
category-valued constants (Note: define is not available in Spad).

Unfortunately www.aldor.org is down :-( again!! ). Perhaps you have a
copy of the pdf version of AUG? If not you can download a version of
it here:

http://www.ph.ed.ac.uk/~bj/paraldor/WWW/docs/documentation/axlugII.pdf

Regards,
Bill Page.