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

[Matthew Fluet]

>> 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).
>
> I don't understand the problem with this approach.  Why can't you
> guarantee that the DB has the necessary theorem, either from an
> earlier invocation of a different executable, or earlier in the
> startup of this executable?

I would have thought that the reason that they didn't want this sort of 
approach is that in addition to having the _code_ for every theory in the 
executable, this would require the _data_ for every theory resident in the 
heap at all times.  That seems like a hefty cost when a user is unlikely 
to touch every theory in a single session.

My suggestion was going to be that they structure things like:

val solve_system =
   fn () =>
   let
     val ADD_COMM = DB "arithmetic" "ADD_COMM"
   in
     fn s =>
     ... ADD_COMM ...
   end

val () = atArithLoad (solve_system, "solve_system")

Where atArithLoad would register the function solve_system with the 
arithmetic theory, so that when a user loaded that theory, the initial 
thunk would be forced (reading the DB, and adding to the heap) and the 
resulting function would be exported to the REPL as the binding 
"solve_system".