[MLton] MLTON_THREAD

Matthew Fluet fluet@cs.cornell.edu
Wed, 18 Aug 2004 10:54:42 -0400 (EDT)


I'd like to propose changing the MLTON_THREAD and MLTON_SIGNAL interfaces
to the following:

signature MLTON_THREAD =
sig

(* the type of threads that expect a value of type 'a *)
type 'a t
(* the type of (user) threads that expect a value of type 'a *)
type 'a u

val new : (unit -> 'a) -> 'a u
val prepend : 'a u * ('b -> 'a) -> 'b u
val freeze : 'a u -> 'a t
val switch : ('a u -> 'b t * 'b) -> 'a
val atomicSwitch : ('a u -> 'b t * 'b) -> 'a

end


signature MLTON_SIGNAL =
sig

structure Thread: MLTON_THREAD
structure Handler:
sig
  type t

  val handler: (unit Thread.t -> unit Thread.t) -> t
end

end


The point is to statically distinguish between explicitly paused threads
and implicitly paused threads.  Explicitly paused threads are ones that
you can arbitrarily prepend to -- in particular, exceptions raised by
prepended code will be handled by the thread.  Implicitly paused threads
can't handle prepended (asynchronous) exceptions.  Even if the prepended
code doesn't raise an exception, it isn't running where you think it is --
it's running before the actual switch rather than after.  Really, the only
thing you can do with an implicitly paused thread is to resume it at
exactly it's paused point.

Similarly, it justifies dropping switch'.  I can't find any uses of
switch' in our code.  Any place where you were using switch', you should
be able to first prepend and then switch -- if you were switch'-ing to an
implicitly paused thread with a non-trivial computation, then it probably
isn't doing what you thought anyways.

In fact, we might go so far as to use the following interface:

signature MLTON_THREAD =
sig

(* the type of threads *)
type t
(* the type of (user) threads that expect a value of type 'a *)
type 'a u

val new : (unit -> 'a) -> 'a u
val prepend : 'a u * ('b -> 'a) -> 'b u
val freeze : unit u -> t
val switch : ('a u -> t) -> 'a
val atomicSwitch : ('a u -> t) -> 'a

end

where you first prepend a thunk to deliver the value, and then freeze.