[Top][All Lists]
[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
- [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure,
Gabriel Dos Reis <=
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/12
- Re: [Axiom-developer] A curious algebra failure, Bill Page, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Bill Page, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/12
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/12
- Re: [Axiom-developer] A curious algebra failure, Bill Page, 2007/08/12
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/12
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), William Sit, 2007/08/12