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

**Matthew Fluet
**
fluet@cs.cornell.edu

*Thu, 31 Mar 2005 21:54:22 -0500 (EST)*

>>* 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".