evaluation order and callcc

Stephen Weeks sweeks@intertrust.com
Wed, 19 Jul 2000 12:18:29 -0700 (PDT)


> Given  ML's  decision that the language (as opposed to the library) semantics
> should be completely nailed down as far as  order  of  evaluation,  shouldn't
> something official be added to the MLton documentation spelling out the order
> of evaluation with regards to callcc (and threads).  Is  this  necessary,  or
> can  I  already  deduce it?

I don't think anything else needs to be said.

>  I was originally worried that MLton might have a
> bug with respect to
>     val a = (1, ???)
> and what the continuation of ??? was.  The point being that it is tempting to
> first   allocate  the  tuple  (before  ???),  but  then  by  re-entering  the
> continuation we could mutate a tuple.  MLton does the right  thing  (although
> it  costs  us  because  it  means that we have to save the result of ??? some
> where else and then copy it into the tuple.

Good point.  MLton does what you say.  I think the only sensible
modification of the Definition to handle callcc (not really doable,
givenm that they are big step, but ...) makes it clear that the tuple
is allocated every time the continuation is thrown to.  Here's a
little example showing the repeated allocation.

open MLton open Cont

val kr: unit Cont.t option ref = ref NONE

val rr: unit ref option ref = ref NONE

val r: unit ref = ref(callcc(fn k => kr := SOME k))

val _ =
   case !rr of
      NONE =>
	 (rr := SOME r
	  ; throw(valOf(!kr), ()))
    | SOME r' => if r = r'
		    then raise Fail "bug"
		 else ()