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

[Page, Bill]

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.

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

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?

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.

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?

BTW, do you know why the (parenthesis) appear the result?

> > 
> > The stuff in interop.boot seems very obscure to me but
> > I am gradually absorbing a little.
> > 
> 
> Yes - it is obscure.  Unfortunately it seemed to be the
> best solution at the time, and then we hacked it about
> a little.  The trick is to try and untangle it again.

Yes.

> There are (at least) two ways domains are treated -
> one is as S-Expression, eg (|List| (|Integer|)) and the
> other is the aldor "Rep2" object - in general axiom code
> handles both, while aldor will only accept the latter.
> 
> > Here's a simple patch that actually prints domain names
> > by calling devaluate() instead of manipulating the domain
> > as a record structure. There must also be something
> > subtly wrong with Rep2?
> > 

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?

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

Thanks for your comments.

Regards,
Bill Page.