[MLton-user] Improved Exn.withEscape

[Vesa Karvonen]

Quoting Stephen Weeks <sweeks at sweeks.com>:
> Being able to return any type is one way to express that a function
> doesn't return.  One way to do this within the SML type system is to
> use a "void" type that has no values.
[...]
> It is certainly easier for the eye to pick out that the passed escape
> function doesn't return when withEscape has the void type.  Compare:
> 
>   val withEscape: (('a -> Void.t) -> 'a) -> 'a
>   val withEscape: (('a -> 'b) -> 'a) -> 'a

    val withLabel : ('a t -> 'a) -> 'a

(Just comparing to withLabel also.)

> With the void type, in order to use the escape function, it is
> essential to have a way to convert the void type to any other type.
> Here's a way.
> 
>   val dead: 'a -> 'b = fn _ => raise Fail "dead"

Yes, I also considered the same basic approach.  A combinator that I
often use when writing new code is undefined:

  fun undefined _ = raise Fail "undefined"

> There isn't a significant difference in client complexity between the
> Exit.withLabel and the withEscape approaches.  Compare the above to:
> 
>   Exit.withLabel (fn l =>
>                   let
>                      val e = fn ? => Exit.exitTo l ?
>                   in
>                      ... e x ... e y ...
>                   end)

Well, I have withLabel and exitTo bound at the top-level for convenience
(although they are not used frequently).  It is quite rare to need multiple
exitTo invocations in a single function so it usually doesn't make sense
to name it like above.

> I think that the void withEscape expresses in the type system the
> properties of what's going on more clearly than the Exit.withLabel
> version.

I'm not so sure about that.  It is well known that the H-M type system
infers polymorphic types for non-terminating terms.  When I look at the
type of exitTo

      val exitTo : 'a t -> 'a -> 'b

It is quite clear to me that it can't return normally.

The withLabel+exitTo approach also parallels the way callcc is often typed
in ML (http://mlton.org/MLtonCont).

> And, it doesn't require a specialized structure with a new
> type and a couple of values to do it.  One does need the Void
> structure and dead function, but those are generally useful for
> expressing the concept of a function not returning -- it seems better
> to use that general concept in lots of places than to create a new
> structure for each place.

That's a better argument, but non-local returns as well as functions that
never return are somewhat of a special case.  The structure where I have
withLabel and exitTo defined also contains other basic combinators so the
overhead you are describing is negligible (or non-existent).

I also worry about the efficiency of the implementation.  The withLabel +
exitTo approach avoids having to build a closure and is likely to yield
slightly better generated code (on any compiler).

-Vesa Karvonen