[MLton] HOL's Moscow ML implementation, and pushing MLton to emulate it

[Michael Norrish]

Stephen Weeks writes:
 
> In this situation, the point is that Michael's goal, I assume, is to
> provide as good an experience to his customers (HOL users) as
> possible.  Hence, it seems worth a fair amount of extra effort on
> his part to eliminate, as much as possible, difficulties in
> transitioning code from scripts to monolith.  It's at least worth
> assessing the relative difficulty of building a MLton-based
> interpreter and a Hamlet-based (or other) interpreter.

This is all true, though I think that moving scripts into the monolith
wouldn't happen that often.  Strictly speaking it would never happen
as scripts are only used to generate theory files (to use the HOL
jargon).  Theory files are data and would never be incorporated
directly into what was compiled, and nor would the scripts.  

But it is certainly true that advanced programmers might test their
ideas out using the scripting interface (which will naturally look a
great deal like the underlying environment).  In this situation, it
would be nice to be confident that they were going to be able to move
from the high-level to the low level with minimal fuss.

On the other hand, Hamlet exists already, and if it is easy to extend,
it would be very tempting to go with the devil we knew rather than the
vapourware we didn't.

As far as extensibility goes, we would particularly like a tool that
enabled us to lift entire ML structures (with their own types and
operations) on them into the interpreted domain, but with the
operations implemented in the interpreter rather than having the
source code interpreted.  We would need to do this with HOL's core
types (term, type, theorem), the parser and pretty-printer, and the
derived elements such as tactics and derived rules of inference.
There are far too many entry-points in all those structures to want to
do this translation by hand.  

These structures' signatures also include a few public datatype
constructors, so Hamlet would have to be able to "see" these as well
as normal functions and values.  I guess such a lifting tool would be
very useful generally...

Michael.