axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] A curious algebra failure


From: Gabriel Dos Reis
Subject: Re: [Axiom-developer] A curious algebra failure
Date: Sat, 11 Aug 2007 20:51:03 -0500 (CDT)

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

As you suggested, I suspect it should have been written like

     if S has SetCategory and S has "*"

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

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

-- Gaby




reply via email to

[Prev in Thread] Current Thread [Next in Thread]