Actually, it's well-known that in the worst case, type checking in ML and Haskell is exponential in the size of the program being checked [though it's usually quasi-linear].  But non-termination appears in other places too - C++ templates are Turing complete too!  Just as we usually write terminating programs, most 'type' functions are (trivially) terminating.  But some of them can be extremely time-consuming.  Even type/polynom, when given complex options, can take a rather long time.

As to your original question: to me it doesn't make sense to compare the strength of those 2 type systems,because they are so fundamentally different.

On the other hand, I would not be surprised if one could embed SK combinators into Axiom's type system, thus showing that it too is Turing-complete.  Apparently Aldor's type-system has been carefully designed so that this is NOT the case. 

Oh, and here's how easy it is in Maple:

`type/crazy` := proc(x) while true do end do; false end proc;

and then type(5,crazy) will send Maple off (the 'false' at the end is not needed, I just wanted to write a proper boolean-valued function, as a type should be).

This is a bit of a non-answer, but I've been waiting for a decent chunk of time to carefully read these posts.  Why?  Because they look like they were carefully composed, and contain non-trivial technical material, so I ought to read them carefully (as opposed to my recent skimming of MaplePrimes material).

So why bother with this comment at all?  Because I really think it's great that there is solid material on MaplePrimes which requires serious reading.  I'm just sad that I am having a hard time getting around to doing the reading!

Static are definitely those checked before run-time -- but saying that that is DAG creation time is too Maple-centric for my taste [even though it's an adequate description].

Maple's static type strength is like Perl's (and python's and PHP's, etc).  Its dynamic type strength on the other hand is essentially off the charts -- dynamic types in Maple are both first class and Turing complete!  First class means they are normal values in the system, and Turing complete means they are arbitrary programs (including some non-terminating ones).  This is way way more powerful than traditional type systems of any kind (static or dynamic).

In the multi-language scenario, it is up to each language to define 'when' its types must be checked, and that forces Maple's hand.  For auto-compiled code, that's going to be the compilation time of that code (whenever that is).

is that there really are now 2 Maple languages, 1d and 2d, which are (unfortunately?) extremely similar.  If they were consistent, then implicit multiplication would be available (or not) in both, which is not the case.

Having 2 languages in the same system is not necessarily bad.  Having 2 languages which have 99% of features in common, now that is something which is a recipe for disaster!  It basically means that you never know if what you learn in one context can be transported to the other (or not).  And since programming is (and should be?) done in 1d, all advanced uses of Maple will be done in 1d. 

Here's the best litmus test for when 2d syntax will have "taken over": when Maple's own library source code is saved fully as document-mode worksheets with all the code in 2d syntax.  Until that's true, I think 2d syntax will remain the one used mostly by newcomers to Maple and eschewed by more advanced users.

Of course, there is a downside to the 2d syntax: for most expressions, it takes more keystrokes to enter than the 1d equivalent (a mouse/palette entry is even less human-time-efficient).

(this should really be in a different thread!)

Different parsers will almost invariably produce different answers.  I would say that the 2D parser's error message here is superior.  [Getting good error messages from a yacc grammar is extremely difficult, and was not expected in the dark ages when it was first created.  Adding better hooks in now to improve this is surely going to be challenging, but nevertheless worthwhile, just to keep up with user expectations].

The typesetting quality has improved in that the images are not randomly cropped so that the image isn't visible, but otherwise the actual quality doesn't seem to have really improved.  The fonts are too small, they're jagged, placement is still sub-optimal, and so on.

Last time I saw a number of these symptoms it was because the fonts were being scaled to a non-natural size.  This is something that, unfortunately, most rendering engines will happily do for you, even though in most instances it's a really serious mistake [don't people who write rendering systems ever read the brilliant works of Knuth on this topic??].  Luckily, in that instance (WebEQ), once it was pointed out to Rob Miner, he fixed it in a couple of days.

That is indeed what programmers think in practice - and such bad habits really hamper them when they try to move amongst a wide variety of languages than just the boring old ones.

The best definition of a 'type' is that a type is "the name of a property that a value possesses".  You may choose to tie your type system to the underlying architecture in a low-level language aimed at embedded systems, but that's not very general purpose.

A weaker type has more values in it because it is a weaker property.  So yes, rtable is weaker than Array with C_order, but that's because of the order relationship in the strength of the properties these names are asserting.

If proc(a::integer[4]) was actually used before execution-time by Maple, then yes, that would indeed be a form of static typing.  But, in the current implementation, it's not [because I can use the same subs trick you did but on the types!).

dsolve({ op(sys), op(IC) });

does work for me, returning quite quickly - but the Eigenvalues are the solution of a degree 4 equation, so indeed generate a nasty mess.  Even with variable renamings (on omega) and generous use of assume, I have not been able to simplify the solution to any great extent.

dsolve({ op(sys), op(IC) });

does work for me, returning quite quickly - but the Eigenvalues are the solution of a degree 4 equation, so indeed generate a nasty mess.  Even with variable renamings (on omega) and generous use of assume, I have not been able to simplify the solution to any great extent.

This basically says that, in Maple, the future intent of any object is unknown until it is actually used.  So a procedure doesn't have to make sense if it's never going to be run as is but used as a template instead.  You can't tell apart templates from procedures, so there is no way to disallow bogus procedures because they might be meaningful templates.

One more comment: Let's all agree that Maple is dynamically typed.  This means that all type checks are done at run-time.  There are tons of such 'dynamic' language -- Python, Ruby, PHP, LISP, Scheme, and many more obscure languages.

Dynamically typed languages force you into "debugging hell" because everything is checked as late as possible.

Statically typed languages make experimentation much more difficult because you're always forced to convince the type-checker (it doesn't need to be a compiler) that what you are writing is meaningful.  Sometimes your program is meaningful, but the type-checker doesn't give you the right tools to 'say so'.  Most often, it's because your thinking is muddled, but it can be extremely frustrating to discover that because of a machine refusing to accept your work.

After quite a few years of experience with both, my conclusion is: if you know what you're doing and are in a known setting, use a statically typed language.  If you're doing something extremely experimental or in a new setting, use a dynamically typed language.  If you are going to do both (and Maple's own library contains great examples of both), then your language should support both paradigms.  That's one of the things I'm currently working on.

These conversions from one representation to another (which imply changes of type as well) are all done at run-time, so 'static' is not really an issue.  [Yes, it also means that the surface type changes, but that's not used by the system in any way].

The only types which are truly 'static' are those which are checked by the kernel at DAG creation time.  Any type which is checked at 'run' time is dynamic.

[for some reason, I did not get any of the notifications from MaplePrimes until yesterday for the last month's worth of posts, so I had missed all these posts.  So sorry for the late reply].

To be more precise, 'static' typing is typing that happens before run-time.  Maple does not do any of this at all - even though it could do some restricted amount.  It already does some restricted amount of simplifications, like

proc() if true then 1 else 2 end if end;

           proc() 1  end

and yet proc() if 5 then 1 else 2 end if end;

           proc() if 5 then 1 else 2 end if end

so why not simply give an error in the second case?  That would correspond to 'static' typing.

To a certain extent, you are correct that surface types are static, because they are assigned by Maple at 'parse time', i.e. when a proper DAG is created.  But it's not really 'static typing' as only very rudimentary checks are made.

Static typing is usually understood to be "early type checking" to eliminate obvious nonsense.  Maple is dynamically typed -- it tells you about obvious nonsense only when it tries to run it and no earlier (with only very very minor exceptions).
 

Typically we say that A is more strongly typed than B is A catches more 'wrong' programs before B does.

I think a Flash-based editor is massive overkill for what's needed! 

Just have 2 tags, one (probably still <maple>) for interpreting direct Maple input and display it nicely [which I am looking forward to] and another (call it <mapleformat> or something, that's not so important) which knows how to interpret whatever gobbledygook Maple sticks onto the clipboard "properly".  And fix Maple if whatever is sticks onto the clipboard is sub-optimal.

That will be much less development work, and surely the web development group has better things to do than to develop a new editor?