[MLton] it is necessary to manually make things tail-recursive?

[Matthew Fluet]

> Lots of HOL code traverses logic-terms in a resolutely
> non-tail-recursive manner.  We were bitten by this recently when a
> user created a list (in the logic) containing 150k elements.  This
> created a very large, and very skewed tree, and we got lots of
> stack-explosions.
...
> But for these large-scale applications, I eventually want to give
> people a HOL implemented in MLton.  So, I was wondering if, for this
> sort of thing at least, MLton is one of those magical compilers that
> sees the potential problems with user code and knows that it should
> make it into an equivalent tail-recursive or CPS form...

There's no specific optimization in MLton that will turn 
non-tail-recursive functions into tail-recursive ones.  I think there is 
some chance that other optimizations will enable a non-tail call to be 
turned into a tail call.  But, for example, we don't try to insert 
accumulating parameters.

Now, MLton heap allocates the ML stack on the ML heap.  So, one can have a 
lot deeper stack than one has in C.  You pay a little in GC time to copy 
the stack to a larger stack when it needs more space.