>>> %5 >> X:Category == with {};
>>>
>>> %6 >> Y:Category := X; () @ Category ... %10 >> z:Type := X; @
>>> Type
>> As you have defined it, X is a category and thus of type Type. Also
>> OK.
> But what is z? It is variable with values in the domain Type. The
> objects of Type are either domains or categories.
After assignment z is a category since z is equal to X. You can also
make z a domain.
%3 >> X: Category == with;
Comp: 10 msec, Interp: 0 msec
%4 >> x: X == add
Defined x @
X with
== add ()
Comp: 0 msec, Interp: 0 msec
%5 >> z: Type := X
() @ Type
Comp: 0 msec, Interp: 0 msec
%6 >> z: Type := x
() @ Type
In any case, I don't see how useful z is, since Type does not export
anything.
>>> %11 >> y has Y T @ Boolean
>> We had that discussion before (and actually also at the Aldor
>> Workshop 2007). Formerly I would have said that should give false.
>> But as Stephen explained it should give true.
>>
>>> %12 >> z has Y T @ Boolean
>> (***) This should be considered a bug. z is a category, so the
>> compiler is fooled by the definition of z: Type == X.
>>
>> Hmm, maybe it's a feature and one can cure the problem with "has"
>> in the definition of "List".
>>
>
> The Aldor Users Guide says:
>
> A ``has'' expression has the following form:
>
> dom has cat
>
> where dom is a domain-valued expression, and cat is a category-valued
> expression.
>
> but perhaps 'has' actually allows dom to be type-valued. So in this
> case, yes I think it could cure the problem with "List Type", except
> that in the current compiler one often gets: "Segmentation fault".
> This I would consider definitely a bug.
I certainly don't rewrite the library to build on such a vague feature
of the compiler. That only calls for more segfaults later.
>>> By "inhabitants" do you mean objects? E.g. the value of Y above?
>> Actually, "object" doesn't say anything. But yes, I consider Y an
>> "inhabitant" of Category, because Y: Category. And I would also
>> consider Y an inhabitant of Type even though you have not
>> explicitly said Y: Type. But any type in Aldor is of type Type.
> I think it is confusing to invent a new name like "inhabitant".
> Object is fairly standard but comes from object-oriented programming.
> In Aldor values do not carry any type information, so they are not
> "objects" in this sense. I would agree to do what the Aldor users
> guide does and use only the term "value". So your "inhabitants" and
> my "objects" are just values of some type.
Good. I can live with that.
>>> For example, in Aldor 'Type' and 'Category' are domains.
>> Sorry, I don't agree. Where have you found that in the AUG?
> See references to AUG and to an article by Stephen Watt at:
> http://axiom-wiki.newsynthesis.org/SandboxTypeDefinitions
I've seen it in Stephen's article. But can you give the exact page
number in the .pdf version of the AUG? Or the exact link to the
information "'Type' and 'Category' are domains".
>>> Objects are related to domains by a membership relation. The
>>> objects of the domain Type are themselves domains (of which Type
>>> is one and Category is another). Categories are subtypes
>>> (subdomains) of Type arranged in a lattice by the inclusion
>>> relation. The objects of the domain Category are these subtypes
>>> of Type (categories).
>> Bill, could you give exact AUG page references for this?
> Just substitute "values" where "objects" occur in the text above. I
> added these definitions from AUG on the web page you created
> mentioned above.
Still, I cannot find this wording in the AUG. Where is it? Searching for
'related' in the .pdf doesn't give too many items. And it's not among them.
>>> So it seems clear to me that all values in Aldor are objects in
>>> some domain, i.e. there are no "category-valued" objects at such
>>> but there are run-time objects of the domain Category and the
>>> domain Type. Still, these objects are treated as category values
>>> and domain values in the appropriate context.
>> Sorry, I don't understand that.
> So it seems clear to me that all values in Aldor are values in some
> domain, i.e. there are no "category-valued" objects at such but there
> are run-time values of the domain Category and the domain Type.
> Still, these valuess are treated as category values and domain values
> in the appropriate context.
>
> Better?
I'd say, no.
If
X: Category == with;
then you don't call X "category-valued"? What happens at run-time is
another question, but this depends on how a compiler implements the
concept of a value of Category. I'd like to understand the relation of
all these names 'Type', 'Category', 'domain', 'Domain', etc. without
referring to an actual "data structure at runtime".
>>> In Axiom (all flavors so far) Type is a category.
>> Reference to such a definition?
> "Type
> a category with no operations or attributes, of which all other
> categories in Axiom are extensions."
>
> from Appendix B of the Axiom book, page 1083.
Hmmm, then why is there Type at all? "with" is exactly such a category.
'Type' is then only another name for "with" and less useful.
However, it is not just another name. Look at the definition of List.
List(T: Type): ...
It would be more restricted to write
List(T: with): ...
since then List would only accept categories as an argument.
>>> The Axiom interpreter automatically creates references to some
>>> types such as 'Domain', and 'SubDomain Domain' but these were not
>>> originally included as built-in domains or domains in the Axiom
>>> library so values of this kind could be implemented only in very
>>> limited ways.
>>>
>>> OpenAxiom introduced Domain as a Domain consisting of all domains
>>> (like Type in Aldor).
>> In my opinion, categories in Aldor are not domains. So I don't
>> agree with "like Type in Aldor", because Type comprises domains and
>> categories.
> In Aldor values of Type are domains and categories. In OpenAxiom as
> it works today values of Domain are domains or categories so that is
> why I said "like Type in Aldor".
OK, I understand. But that makes the world more complicated.
In Aldor:
We certainly agree that any aldor-type has the type 'Type'.
So that is fine (concerning the *name* 'Type').
In OpenAxiom:
Every domain has type 'Domain'. Fine.
Every category has type 'Category'. Fine.
But also every category has type 'Domain'. That is not so nice.
>>> OpenAxiom also adds 'Category' as an alternative to 'SubDomain
>>> Domain'.
>> Really? Gaby, does that mean that in OpenAxiom a category is
>> (conceptually) a domain? I don't speak of implementation details
>> here. That one can (perhaps) implement categories and domains (by
>> the latter I mean the collection of all things of type C where C is
>> any category) by the same data structure and find a common name for
>> that data structure. But I would find it confusing if that concept
>> is also called "domain".
>>
>
> Aldor uses the name 'Type' for the domain (data structure) that
> includes both domains and categories.
Ooops. Who told you that the internal data structures of domains and
categories are the same in the one and only Aldor compiler.
> In Axiom Type refers to the category as referenced above. So either
> this has to change or OpenAxiom needs some other name for the domain.
> Using the name 'Domain' does not seem all that confusing to me. Then
> a 'Domain' is the only thing in the system that represents a user
> accessible data structure of some kind. To say that
>
> - Domain is a Domain - Category is a Domain - Type is a Category
>
> is perhaps simpler than Aldor's
>
> - Domain is a Type - Category is a Type - Type is a Domain
Who knows? I somehow start thinking that all this discussion has 'the
implementation of reflection' as its background. True?
>> Gaby, what do you consider to be a domain? Such a data structure
>> concept or simply something that has a category as its type?
> In Axiom a domain is still something that has a category as its type
> because categories are subdomains of Domain (just like categories are
> subtypes of Type in Aldor).
>>> I believe that the intention of OpenAxiom is that Category is a
>>> domain however it is not always treated that way in the current
>>> revision.
>> Again, that is confusing to me. Is it possible to choose some other
>> name for that? "domain" should not be as meaningless as object is
>> nowadays.
>>
>
> The concept of "domain" still seems clear to me. That is another
> reason why I do not particularly like the idea of using "Domain" as
> the top of the category hierarchy - that is confusing unless you
> realize how these terms are used differently in Axiom and Aldor.
>
>>>> where in my notation above "Domain" should just be considered
>>>> the top of the category hierarchy. (Actually, the top is
>>>> "with", I just named it "Domain").
>>> Names are significant for named categories. Categories reference
>>> other categories by name. 'Category' is the domain of all
>>> categories. It's objects are categories.
>> If you had written "'Category' is the class of all categories.", I
>> would relax. But you used "domain" and that confuses me.
>
> Is it better if I said: "It's values are categories."?
"It's" refers to what? If you mean "values of Category are called
categories", I relax, since that is the same as saying "a category has
'Category' as its type".
>> Let us clarify. I have started with my definitions on
>>
>> http://axiom-wiki.newsynthesis.org/SandboxTypeDefinitions
>>
>> Add yours.
> Do you mean "add my proposal for how this should work in OpenAxiom"
> or my understanding of how it works now in Aldor? (I have already
> done the latter.)
What I mean is to define *your* use of those concepts. So that whenever
'domain', 'Domain', 'Type', etc. appears in a mail from you, I can
always go to the page above and look up your definition.
I'd like to record the status so that we understand each other better.
So there should actually be no reference to Aldor or panAxiom.
If you have proposals for a better future, write them down, too, but
mark it as "Proposal".
Ralf
-------------------------------------------------------------------------
Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW!
Studies have shown that voting for your favorite open source project,
along with a healthy diet, reduces your potential for chronic lameness
and boredom. Vote Now at http://www.sourceforge.net/community/cca08
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
