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

[Michael Norrish]

Matthew Fluet writes:
 
> Scott has the right idea, but one can make it more formal (and more
> extensible) by using the ideas of embedded interpreters.  See, for
> instance,
 
> http://www.eecs.harvard.edu/~nr/pubs/embed-abstract.html

> and

> http://research.microsoft.com/~nick/benton03.pdf

I've looked at both of these papers, and am tempted to say that we
need the ideas in them because they're obviously way cool.  However, I
suspect that we don't need to implement a programming, or "scripting"
language at all.  Indeed, expressing proofs as programs is arguably a
mistake, and we should be providing a proof language that is not
programmable at all.

Splitting the programming of proof procedures from the day-to-day
writing of proofs happens by convention anyway: the day-to-day proofs
are 90+% programming free and use a very restricted set of base
operations and connectives.
 
> > -- Creating a monolith ----------
> >
> > To create a MLton-based, possibly interactive system, supporting the
> > various special-purpose bits of code we've written, it seems we will
> > have to do the following:
> >
> > * change to use a data-file format for theorems on disk
> > * implement our own proof language
> > * eventually build one monolithic executable that includes all of the
> >   code that accompanies various theories.  For example, the code for
> >   deciding linear arithmetic over the real numbers will always be
> >   present, even if the user is only working with sets of natural
> >   numbers.
 
> You are paying some executable size and possibly persistent heap
> usage, but I don't see other negatives for having all the code in
> one executable.  You could certainly implement some sort of
> name-space management in your interpreter/proof-language so that
> various bits of code weren't available until the user loaded the
> appropriate theory.

I think you're right, but I'm curious as to what you think is the
right way to do this.  For example, our current linear arithmetic code
might look like

structure LinArith = struct
 
  fun solve_system s = .... arithmeticTheory.ADD_COMM ....

end

The code for solving a system of linear equations uses the fact that
addition is commutative, which fact is embodied in the theorem
ADD_COMM from the theory of arithmetic.  Now, if theories are just
data files, then we can assume that loading them from disk populates
some central database, and the above might become

  fun solve_system s = .... (DB "arithmetic" "ADD_COMM") ....

If this code somehow ends up being called where the theory of
arithmetic is not in the context, DB will generate some exception, and
all will be well.  Semantically, this is fine, but I don't much like
the prospect of repeatedly having to query the database each time this
is called (real code will depend on a number of different theorems).
I'd really like to write

  val ADD_COMM = DB "arithmetic" "ADD_COMM"
  fun solve_system s = .... ADD_COM ....

But this won't work because the binding for ADD_COMM will happen as
the executable starts up, in an arithmetic-free context, and DB will
raise an exception.  (We need to support such a context precisely so
that our tool can itself be used for the development of the arithmetic
theory in the first place).  In a situation where code can be
dynamically loaded, we could ensure that the above was only loaded
when it would work, by loading it after the aritmetic theory data was
loaded.

But in the proposed monolith, do we have to produce something like:

  val initp = ref false
  val func = ref (fn s => raise Fail "Uninitialised")
  fun real_solve_system AC s = .... AC ....

  fun solve_system s = 
    if !initp then !func s
    else 
      let val ADD_COMM = DB "arithmetic" "ADD_COMM"
      in
          initp := true;
          func := real_solve_system ADD_COMM;
          !func s
      end

or something equally revolting?

Moreover, what do we do with direct value (not function) bindings that
might depend on our database?  (I'm pretty sure such bindings exist in
our code base.) The reference to arithmeticTheory's ADD_COMM could be
hidden inside a lambda-abstraction above, but if our code is

  val myvalue = .... arithmeticTheory.ADD_COMM ....

what do we convert this to?

Is there some good way of doing this 'delayed initialisation' (for
want of a better term)?  

Incidentally, I suppose that pushing this sort of code into an
embedded interpreter would be a solution to the staging problem.  The
problems are that the interpreter would have to cope with next to all
of SML, and it would lose us precisely the sorts of efficiency gains
we'd hope to get by moving to MLton.
 
Thanks for your comments so far!

Michael.