[MLton] HOL's Moscow ML implementation, and pushing MLton to
Wed, 6 Apr 2005 11:59:16 -0700
> > Because of differences between SML implementations
> > (mostly libraries, but sometimes language too), it may thus make the
> > most sense for the embedded interpreter to use MLton's front-end and
> > libraries.
> Do you really think so?
> Aren't you essentially saying that the standard (for language and
> library) is mostly useless then?
No. It makes it *much* easier to port programs than it would be
otherwise, perhaps even making it possible in some situations where it
would be impossible otherwise. However, it's still a lot more
difficult to port between SML/NJ and MLton, say, than it is between
MLton and MLton :-).
> You are assuming that any non-trivial program will likely touch
> non-portable corners of the language. I don't believe that's the
> case, and I would consider it a disastrous situation for a standard
The situation isn't disastrous; it's just difficult to do as well as
the ideal (no porting effort at all). Like I said, the porting issues
are mostly libraries, but sometimes language too. As to libraries
there is the problem that different SML implementations provide
different modules (e.g. MLton has Int64 but Hamlet does not) and that
different modules have different meanings (e.g. in MLton, Int is
Int32, while in SML/NJ, Int is Int31). Also, the rigor of the basis
library spec is (unavoidably) a notch below that of the language spec.
As to the language, there are the corners where the language allows
flexibility, like the scope of resolution of flexible record patterns
and constants. I run into all of those when porting.
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.