Lambda the Ultimate

What I wonder now is how Axiom and Aldor compare to, say, David McAllester's Ontic.

;--)

The Ontic language in its latest incarnation is basically a new syntax for ZFC. As such, it is an untyped language--there is nothing to prevent you from attempting to treat a function as a natural number, except that it will be difficult to prove facts about such a construct. The Ontic system is a proof verification system, rather than a computer algebra system.

If people have questions about Ontic, I'll try to answer them.

http://page.axiom-developer.org/zope/Plone/refs/

If you are interested in AXIOM, please feel free to join and look around.

Aldor's online documentation is pretty good; see orientation and types. Frank will appreciate that only minimal types are built-ins. The Axiom documentation is sparse, and I am not clear on the relation between the two.

From that nice portal site, an excerpt from A First Report on the A# Compiler (no, it's not .NET):

From a compiler implementation perspective, the most interesting aspects of the A# compiler are:

• type inference in the context of overloaded identifiers and type constructors, with types being first class values,
• the combination of cross-file inlining and data structure elimination to reduce overhead,
• the use of dataflow analysis to reduce flow graphs produced by constructs such as generators,
• efficient implementation of types as run-time values,
• storage management performed through a run-time conservative garbage collector, and
• portability across many hardware platforms and operating systems.

As far as we are aware, the first three of these items are new. The remaining items have novel aspects....

A major part of the A# compiler is concerned with producing optimized intermediate code, or Foam code. "Foam" is an acronym for "First Order Abstract Machine." The abstract machine is first order in the sense that it does not treat its types as values. Foam is designed to contain only those concepts which can have an efficient realization in both Lisp and C [although]...Foam is not restricted to the precise intersection of C and Lisp....Presently, only C and Lisp code are generated directly from Foam.

Wonderful as all this sounds, it is also ten years old. Are there any more recent papers on the whole Axiom world? These folks were ahead of their time. Maybe with the code now open-sourced, the future is even brighter.

On a more personal note I would be interested to hear comparisons with Mathematica (v5) from both philosophical and user standpoints. Mathematica also puts symbolic computation on an equal footing with numeric computation. Not all systems do that.

With Tim Daly's permission I will quote him:

Axiom is a full general purpose programming language with the property that type selection is based both on the function signature and the return type. So you can write:

Integer foo(x:Integer)
Float foo(x:Integer)
etc

The strength of Axiom lies in the library. It is about as close as you can get to the mathematics you want to write. The strong typing appears to be "in the way" until you realize that, since you are forced to think thru the type issues, you write code that is likely correct when it finally runs.

Aldor == A# == AxiomXL (these were various names that the language used at various times but were changed for historical reasons).

Axiom is written in common lisp. There is a programming language for Axiom called Spad. At one point we (I'm one of the original axiom authors) decided to "clean up the compiler and the language". Stephen Watt decided to implement the "new6 compiler" in C as an external program. So parallel development and improvements were made to the Spad language in common lisp and C. The two compilers accept the same language modulo a bunch of "stand alone" issues like libraries, I/O, etc. So they are the same language.

Axiom can use Aldor programs easily but Aldor because Axiom is a whole environment and the Aldor programs just get loaded and linked. Aldor standalone programs cannot use the Axiom library because the require common lisp.

Axiom has lived in about 8 different lisps, including MacLisp and VMLisp/370, Symbolics Common Lisp, etc. A scheme port could be done but you'd end up writing a lot of common lisp functions, which are really re-implementation of missing VMLisp functions, which are really re-implementations of missing MacLisp functions. See the source code where I've commented on the rewrites I did while porting. I could move it to scheme, but really, why?

Haskell doesn't add anything to Axiom as all of the concepts are already available so the Haskell port would just be another reimplementation (albeit quite harder because of the semantic distance).

Tim