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

Daniel C. Wang danwang@CS.Princeton.EDU
Fri, 08 Apr 2005 17:18:15 -0400


Stephen Weeks wrote:
{stuff deleted}
> But, as far as I understand, it doesn't show how to
> leave the host types fully unboxed with an open-ended interpreter as
> we want.  Although perhaps its reference to type passing as being at
> the other end of the spectrum from coercion is a hint that type
> passing might work.

My memory is a bit sketchy, but as I recall Shao's approach assuems a native 
  unboxed/host representation. The trick is to carefully insert *partial* 
boxing/unboxing operations when coercing between monmorphic and polymorphic 
contexts. The partially boxed universal rep is basically a pointer to the 
underlying unboxed native rep.

In our context this requires rewritting the interpter to use the paritally 
boxed universal rep.


For example here's how the paritally unboxed approach differs from the fully 
boxed approach.
signature U = sig
    type 'a univ

   (* partially boxed approach *)
   (* NONE == [], SOME(x,xs) == x::xs) *)
    val unwrapList : ('a list) univ -> ('a * 'a list univ) option

   (* fully boxed approach *)
    val unwrapList' : ('a list) univ -> 'a list

  end

(* paritally boxed approach *)
fun univLength (NONE) = 0
   | univLength (SOME(_,xs)) = univLength (unwrapList xs)

(* fully boxed approach *)
val univLength = length o unwrapList'


In the partially boxed approach each boxing or unboxing operation is 
constant time, because we only box the toplevel structure.