[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.