RE: [Axiom-developer] types as values, and type internals

[Peter Broadbery]

On Thu, 2005-09-29 at 17:48 -0400, Page, Bill wrote:
> On Thursday, September 29, 2005 3:21 PM Peter Broadbery wrote:
> > ... 
> > It was written mostly to show that you could do some
> > operations on domains - effectively allowing one to write
> > more of an interpreter in the extension language.  I'm not
> > 100% confident of what the definitions of "Domain",
> > "SubDomain", "Category" and "Type" should be, so was
> > avoiding them.
> 
> It seems that that might have been the prevailing approach
> in the latter stages of Axiom's development - a pity
> considering Axiom's otherwise quite noble objectives
> concerning mathematical rigor. ;) Seriously, this issue
> does give me a headache that I would like to releave.
> 

It has given me the odd headache too - worries about the upper levels of
the type hierarchies came up rarely, and there was often some more
pressing thing to worry about.

> > 
> > If we can find a way that these can fit together and allow 
> > axiom to deal with them coherently it would definitely be
> > a good thing, but I'm not sure I'm qualified to decide
> > exactly what the semantics should be.
> 
> I agree that it would be a very good thing, but if you are
> not sure you are qualified, then I am not sure that I am
> even qualified to have an opinion! :)
> 

I just wrote bits of the compiler - the type hierarchy conveniently goes
away when you're worrying about code generation.  Below is some
speculation - I have not verified it against any real documentation or
code.

Just as an idea, we could explain things this way:
The 'is a type of' (ie. a: A) operation in aldor is slightly overloaded
- in the context of a domain, 'A', it says that 'a' is represented as
specifed in the domain, and that when '%' appears in the signature of
one of the operations, then a can be used there.  In the context of a
category, it means that 'a' implements the operations exported by 'A'.

As an aside, one could consider writing a language which has separate
syntaxes for these.  You could also argue that java's 'implements'
keyword is the equivalent of : at category level, but that'll be another
argument. 

Anyway, from this point of view, the type of domains is 'domain',
implementing your favourite Domain-level functions (eg. name,
findExport), while Categories are objects which mostly list exports
(they also supply default operations, but I'll ignore that).  The
operations on a category object are different - findExport makes no
sense without an underlying domain implementing the operation.  So,
you're left with 'name'(*).

Now we could if we wanted to take this to a logical extreme, implement a
category of domains, and thus allow the user to have entirely different
representations for types in the same system, and all respecting the
category hierarchy.  Luckily, (although unfortunately for asprin
manufacturers), axiom hasn't quite done this.  Instead, we have the type
of "domains" - Domain, and the type of things that list operations
returned by getOperation (ie. Categories), which must be 'SubDomain'.

This may be close to the original intention - some older timers may want
to chime in here.  It doesn't really explain 'Type' particularly, and in
fact it may be that 'Domain' was an experiment which was at least
partially supplanted by the (initially simpler) idea of a two level type
hierarchy.

(*) In fact, categories implement name, and functions for reading the
parent categories, and also behave like domains (so you can instatiate
them to get defaults).

> > 
> > > I wonder if the Rep == Type really makes sense?
> > > 
> > 
> > I think Rep ==> Type is more or less honest, given that
> > a Type is an object in the aldor world view. A caveat is
> > that it captures  categories (and "Type") as well as domains.
> 
> Hmmm. Ok so when I am writing Aldor code in Axiom I (for
> the most part) have this "aldor world view", right? So Type
> is something native to Aldor?
> 
> In the Axiom interpret if I write:
> 
>   (1) -> Type
> 
>      (1)  Type
>                                      Type: SubDomain Domain
> 
> It answers with a Type for Type that is hard for me to
> understand ... especially considering that the Axiom Book
> specifically says that the Type of Type is undefined. :(
> 

Even if it is undefined, it has to have a value.  I'm guessing that
saying 'undefined' gives an opportunity to redesign and still be
correctly documented.

> Anyway, am I correct then to understand that
> 
>    Rep ==> Type
> 
> here means that we are going to 'pretend' about something
> that is assumed to have a structure directly understood
> by Aldor? Doesn't that mean that anything like:
> 
>           name(t: %): SExpression == {
>   -               dom := t pretend Rep2;
>   -               axiomName((dom.v.domName)(dom.o))
>   +               dom := t pretend SExpression;
>   +               devaluate(dom);
> 
> that just pretends that something passed from Axiom has
> such a structure would be rather dangerous? Instead we
> would have to ask Axiom to do some kind of explicit
> conversion to the Rep2 structure, right? Perhaps that
> explains why the original code for name above (-) failed?
> 

It's expecting an (aldor) domain, and it appears that mappings seem to
be represented differently.  I'd need to sit down with a debugger for a
while before answering further, I think.

> Notice how many question marks I wrote in the above
> paragraph? :) That's how certain I am about all this
> so please forgive me if my writing seems overly pedantic.
> 

I'm not 100% sure of anything, which is why I can't really be too
confident.

> Given that in the AldorDomain code you write:
> 
>    theIntegerType(): % == per Integer;
> 
> what is the difference in the interpreter when I write:
> 
>   (1) -> A:=Integer
> 
>      (1)  Integer
>                                            Type: Domain
>   (2) -> B:=theIntegerType()
> 
>      (2)  (Integer)
>                                         Type: AldorDomain
> 
> Is there a difference in the internal representations?
> 

I think they have the same representation - you can check by tracing
'recordAndPrint', or looking for where axiom stores its result history.
They have different types, so print differently, I think (cf. Integer
and RomanNumeral for a more obvious example).

> Aha. See my question above about name function. So I guess
> it is just a matter of knowing which sturcture to use
> and when to convert, right?
> 

Yes - though I think the older representation should not be leaking into
the aldor world, and this might be the bug.

> > 
> > Devaluate should be equivalent for all domains.  Ah,
> > Mappings aren't quite domains, since  'isDomain' fails
> > for them. Not sure what the underlying bug is though.
> 
> If I write Domain instead of AldorDomain in your code and
> compile it then I can write
> 
>   (1) -> (Integer, Float)
> 
>      (1)  [(Integer),(Float)]
>                                         Type: Tuple Domain
> 
>   (2) -> ((Integer->Float),(Float->Integer))
> 
>      (2)  [(Mapping (Float) (Integer)),
>                     (Mapping (Integer) (Float))]
>                                         Type: Tuple Domain
> 
> it looks as if Mapping is understood by the interpreter but
> the coerce to OutputForm from Tuple doesn't seem to be doing
> such a good job.
> 

The coerce in Tuple is fine - I think your expectations of devaluate
aren't right - what your seeing in AldorDomain's coerce is the axiom
representation of the type, which is not the same as its print
representation.

Hope this helps. 

Pete

> Thanks for your comments.
> 
> Regards,
> Bill Page.
-- 
Peter Broadbery <address@hidden>