[Axiom-developer] Axiom interactive input syntax (was: [Axiom-mail] RE: AXIOM / TeXmacs problems(bugs?))

[Bill Page]

On Monday, December 08, 2003 2:01 PM David MENTRE
wrote:

> 
> Another approach might to use only a compiler, the 
> "interpreter" just feeding input to the compiler and 
> displaying its output. This is the approach followed in
> the Objective Caml language.

There is also a mode like this in Aldor, the Axiom library
compiler. But compared to the Axiom interpreter it seems
very awkward. Maybe a TeXmacs - Aldor interface would help.
I wonder if anyone has done this yet? I imagine that some
people might already use emacs with Aldor in this way.
 
> 
> Such a design would raise the issue of having a good type 
> inference algorithm that would allow (1) a light syntax
> (an absolute necessity for the interactive mode) and
> (2) would be, at the same time, a unique, well defined and
> correct type inference.

That is certainly the hard part! <grin>

> From the few pages I have read in the Jenks & Sutor book,
> the "label" type inference (or "record" type inference) as
> found in the Objective Caml language and used for the typing
> of objects (as in object-oriented) might be sufficient. But
> clearly more work would be necessary to have a light syntax
> in interactive mode[1].

That is interesting but compared to what we were discussing
originally about unifying the Axiom interactive input language
syntax with the compiler language syntax - this is what I
would call *very* ambitious.

What I had in mind was much simpler. I thought it might be
useful to modify the TeXmacs/Axiom (tm_axiom) interface
program so that it stores what it gets from TeXmacs (when
you press Enter) into a temporary text file, say
/tmp/texmacs.input, interpreting shift-Enter as new lines,
and then calls Axiom with

 )read /tmp/texmacs.input

to execute the commands. This would allow the usual indented
block structure style to be used rather than the ( ) block
structure. And the syntax would then be closer to the
compiler syntax and also essentially identical to the code
that is displayed in the Jenks & Sutor book.

This change is simple so when I have a moment, I will try
it. But I am not sure that it will always work nor whether
it is the best approach.

> 
> Yours,
> d.
> 
> [1] In short, in ML like languages, the type of objects is 
> deduced from the name of the operator (e.g. '+' has
> '(INT, INT) -> INT' signature, using Axiom notation). In
> Axiom, it appears to me that typing is more object-oriented
> like, in the same way as SmallTalk or C++ with overloading:
> the type of objects determines the type of operation to apply.

Yes, that is exactly true. Notice that in interactive Axiom
when we define

  f(x) == x+x

we have not really defined a function yet. It is only a kind
of template for a class of functions. (I am not sure of the
correct technical Axiom term of this.) It is only when I write

  f(2)

that Axiom compiles a function of type

  Integer -> Integer

It is during compilation that + is identified as +$Integer,
although I could have been more specific, if I so choose,
when I wrote the function "template" and included more type
information - the way I would have to if I was writing and
compiling a library routine.

Then when I write

  m := matrix [[1.0,2.0],[3.0,4.0]]
  f(m)

Axiom compiles another function of type

  Matrix Float -> Matrix Float

etc. So even in an online session we might have several
different functions associated with the overloaded name f.

> One might envision a typing system where you have several
> operators ('+int' for (INT, INT) -> INT, '+poly' for
> (POLY, POLY) -> POLY) (thus you can use ML-like type 
> inference) but hide those several operators with some
> "hints" from the typing of previous objects in interactive
> mode (e.g. x is a POLY, so the '+' in "x+3" means
> "use the '+poly'"). I don't know yet if this idea is
> just smoke in my brain or a real good idea. :)

Not at all. That is (more or less) exactly how Axiom works
now. See "package calling" in Jenks and Sutor, page 83.

Regards,
Bill Page.