[MLton] HOL's Moscow ML implementation, and pushing MLton to
Daniel C. Wang
Mon, 11 Apr 2005 18:31:38 -0400
Stephen Weeks wrote:
>>Attached is SML file that sketchs how to do the interoperation
>>expressed as a source to source translation of code to be linked
>>into the interpter.
>>It deals with recursive polymorphic structures. Each coercion
>>between the generic and hosted representation is constant time.
> Thanks for the code Dan. It made sense. Here's my take on what it
> does, and does not, do, followed by an attempt to improve on it.
okay, I think we are on the same page now.. :) so all your complaints make
> Now, for some drawbacks.
> Abstracting code to deal with different representations of lists has
> the effect of adding an additional amount of polymorphism to all of
> the code, whether it was originally polymorphic or monomorphic. For
> example, consider the Lst.sum code. Initially, its type is
> val sum: int list -> int
> After translation, it becomes Lst.sumF, and its type become
> val sumF: ('a -> (int, 'a) listF) -> (int, 'a) listF -> int
> Of course, this polymorphism is essential to be able deal with the
> different representation of host lists and hosted lists. But its
> cost, in the context of MLton, is that all the host code that deals
> with the interpreter, including monomorphic code, is duplicated. In
> MLton, we're used to duplicating polymorphic code. Duplicating
> monomorphic code is a new thing, and it would be nice if it could be
> avoided (or at least we had a choice so we could make a compile-time
True, but I suspect it won't be as bad. If we actually, only duplicate based
on the underlying representation type and not source level type. i.e. All,
objects with a boxed representation share the same code. Even if they are
used at different types. Given what I remember of how MLton is constructed,
I can see that even this might be a major change.
> Your approach is very similar to copying the entire program and
> feeding it as source to the interpreter, and then running parallel
> dual worlds -- there really isn't much communication between the
> worlds. There is an advantage of your approach in that the source of
> the exported functions is compiled by MLton, but they're still
> dealing exclusively with the hosted universal datatype.
Well, the host code is now sufficiently generic that it can deal with any
representation. It just happens to be the one used by the interpreter.
> One thing I would like to see in a solution is that if I define a list
> and a sum function in the host world
> val xs: int list
> val sum: int list -> int
> and export both of these to the hosted world, and then in the hosted
> world call "sum xs", it should effectively call "sum xs" in the host
> world. This will give one the freedom to experiment in the hosted
> world while getting a lot of the speed and representation benefits of
> the host world.
Here,I'm a little lost. It seems like once you pass "sum" xs to the
interpter it escapes. So that there's less you can realy do wrt to
> Your solution doesn't achieve this (not that I'm
> claiming that you could know that I wanted it :-). Your solution will
> (lazily) coerce the int list to the universal type, and apply the
> duplicate copy of sum for the hosted world, which deals only with the
> universal type.
Okay, this is accurate.. so whatever you are complaining about. I have to
agree it is true. :)
> The only real communication between the worlds is the delaying trick
> that allows constant-time coercion of host values to hosted values.
> Unfortunately, there is *no* communication the other direction. The
> delaying trick doesn't work, because there are no hooks in the host
> types to introduce delaying, and I want to avoid changing host
> representations because that would adversely affect host performance.
I could do without the delaying trick if I had existential types in the
source language. :)
> Unfortunately, communication from hosted world to host world is
> essential. Suppose we had a variant of Lst.sum that saved its
> argument in a ref cell.
> val r: int list ref = ref 
> val sumSave: int list -> int = fn l => (r := l; sum l)
> Duplicating the ref cell is not an option (it is semantically
> incorrect), and abstracting sumSave over the representation of lists
> doesn't help. When sumSave is called in the hosted world, the only
> choice is to completely coerce a hosted list to a host list. If the
> hosted world represents int lists by embedding them piece-by-piece
> into a universal datatype, then this will obviously not be a
> constant-time operation. Things are even worse if the data structure
> is more complicated than a list and contains mutable components of its
I had thought about ref cells a bit too. The right way to deal with this is
to abstract the interface of a ref cell as setters and getters.
> My conclusion is that for a complete and efficient solution, one must
> embed host values directly, not piece-by-piece, in the hosted
> universal datatype. Then, coercions both ways are trivially constant
> time; either add a tag or remove it.
> I'm not certain that this works for all of SML, but I am hopeful. I
> think we may have been able to go beyond where Nick went in his paper
> because of the use of recursion schemes, type passing, and the use of
> one variant per monotype in the universal datatype.
Someone should get ambitious and write this up for the upcomming ML
workshop. Once a good solution is figured out.
So here is a summary of the two approaches. ..
The basic gist of my idea is to recompile all the code that deal with both
universal and native values in as abstract way as possible. So it doesn't
care how things are represented. What you are suggesting is to recompile all
the code so it all deals with one concrete representation.
Both our approaches lead to different kinds of performance problems. My
approach allows you to use any representation you like, but you take a
performance hit in that code that deals with both hosted or host values has
to access that code through an abstract interface.
Your approach dictates a universal rep so potentially all code pays a
performance hit. However, it is admitly simpler, and fits within the MLton
whole program philisophy.
On the face of it. It's not clear what is better. I suspect doing the
obvious simple thing first.. is always the right way to go... but if things
hit a performance wall.. I think its worth investigating the other approach.
I think, the real deciding factor is how values move across the host/hosted
worlds. If they really agressively share values then one big concrete type
is probably the best way to go.. if there's little interaction paying the
abstraction hit might be better for overall performance.