Dear Stephen,
could you clarify (***)? Thank you.
On 07/08/2008 05:05 AM, Bill Page wrote:
> On Sat, Jul 5, 2008 at 2:38 AM, Ralf Hemmecke wrote:
>> ...
>>>> then I would (roughly) say that
>>>>
>>>> Type = Category + Domain + {Type}
>>>>
>>>> i.e. Type comprises all categories, all domains and itself. The constant
>>>> 'Category' (which is a keyword) is on the same level as 'Type' but with
>>>> less inhabitants than 'Type'.
> What do you mean by "'Category' which is a keyword"? Do you mean that
> it is built-in?
Of course, Category is built-in. That there is a definition like
Category: with == add;
in sal_lang.as does not say that it is not built-in. Also Boolean is
built-in. And still the Aldor compiler *requires* a definition like
Boolean: with == add;
since otherwise it will not work properly. Don't ask me why the
designers of the Aldor compiler did it in such a way that something like
sal_lang.as is required to compile anything useful at all.
The meaning of "Category" is as in Doye's thesis.
(Section 2.5 of
http://axiom-portal.newsynthesis.org/refs/articles/doye-aldor-phd.pdf/?searchterm=doye)
> In that case I would not agree. In Aldor for example:
>
> %1 >> #include "aldor"
> Comp: 60 msec, Interp: 0 msec
> %2 >> #include "aldorinterp"
> Comp: 20 msec, Interp: 0 msec
> %3 >> Category
> () @
> with
> == add ()
>
> Comp: 0 msec, Interp: 0 msec
> %4 >> Type
> () @
> with
> == add ()
Well that is as the definition in sal_lang.as, but still there is
special treatment for them inside the compiler. And I don't think that
output proves anything.
Aldor does also allow me to compile
---BEGIN aaa.as
#include "aldor"
extend Category: with {foo: () -> Integer} == add {foo(): Integer == 1}
-- import from Character, Integer, TextWriter;
-- stdout << foo()$Category << newline;
---END aaa.as
the only problem I have with that is that I don't know how to interpret
it. In fact, I have the suspicion that the "Category" that prints like
"with==add" is actually not usable at all. Uncomment the lines above and try
aldor -fx aaa.as
My version of the compiler tells me
"aaa.as", line 4: stdout << foo()$Category << newline;
...............^
[L4 C16] #1 (Error) There are no suitable meanings for the operator
`foo$Category'.
If Category really were treated as a domain that should not happen.
I just think that a user should actually never see sal_lang.as, because
it is misleading.
> %5 >> X:Category == with {};
> %6 >> Y:Category := X;
> () @ Category
Fine. And Y is, of course not any different from X ...
> %7 >> x:X == add {};
> Defined x @
> X with
> == add ()
> %8 >> x has Y
> T @ Boolean
... therefore that is OK, too.
> %9 >> y:Type := x;
> @ Type
As you have defined it, x is a domain and thus a type, i.e. something of
type Type. So that is also OK.
> %10 >> z:Type := X;
> @ Type
As you have defined it, X is a category and thus of type Type. Also OK.
> %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".
> 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.
>> Bill Page wrote:
>>> I don't like this much since it seems to conflict with the actual
>>> usage of these terms in both Axiom and Aldor.
>> Why do you see a conflict here? Is, what I say, not what Doye
>> says in Section 2.5 of
>> http://axiom-portal.newsynthesis.org/refs/articles/doye-aldor-phd.pdf/?searchterm=doye
>> ?
>>
>> items \in Domains \in Categories \in Category
> Perhaps it is almost ok if you include Doye's notation Obj(...)
I have no problem with that.
> but this ignores the concept of Categories as subtypes of Type.
> If 'x has X' implies 'x has Y' for all x in Type then X is a subcategory of Y.
Where do you see a problem here? Which "has" is it? In Aldor you must a
domain in front of "has" and a category behind. You only get problems if
you consider Type to be a domain and accept (the bug) that "z has Y"
should give true.
> Between Axiom and Aldor the terminology is such a mess that it is hard
> to say anything in a simple manner without defining everything from
> basic principles.
Maybe we should start writing Aldor-has, OpenAxiom-has, etc.
Aldor-Category, OpenAxiom-Category. ;-) at least it would clarify a bit
more.
> For example, in Aldor 'Type' and 'Category' are domains.
Sorry, I don't agree. Where have you found that in the AUG? I don't
accept compiler output as an argument.
> 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?
> 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.
> In Axiom (all flavors so far) Type is a category.
Reference to such a definition?
> 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.
> 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".
Gaby, what do you consider to be a domain? Such a data structure concept
or simply something that has a category as its type?
> 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.
>> 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 OpenAxiom going to somehow blur the distinction between categories and
>> domains?
> If Aldor treats categories and domains as first order doesn't this
> already blur the distinction?
Not for me.
> Although domains are never objects of Category, both categories and
> domains are objects of Type.
There is no problem with that. Or do you see one?
>> I understand that it would be nice to really use categories as first class
>> objects, but that does not mean that they must be considered as domains.
>> Or does it?
> Yes, I think it does.
No, it doesn't. What you want, is that categories and domains (by the
latter I mean the collection of all things of type C where C is any
category) are treated in the same way (first class objects). So that is
more in the sense of a common data structure that I mentioned above. I
have no problem with that common treatment, but please don't call it
"domain". Maybe call it "class" or "magma" or whatever, but not "domain".
Let us clarify. I have started with my definitions on
http://axiom-wiki.newsynthesis.org/SandboxTypeDefinitions
Add yours.
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
