[MLton] Question about Definition of SML :)

[Anoq of the Sun]

Stephen Weeks wrote:
> And of course all of this only holds at the top level.  I don't think
> anyone would argue that the following program can be rejected.
> 
>         val _ =
>            let
>               val x = ref nil
>               val _ = 1 :: !x
>            in
>               ()
>            end

Just a comment here - maybe I didn't understand the nested declarations yet.

Do you mean to say that it's OK if this program is rejected or that it should
certainly not be rejected? (I'm just not sure about your 2-line description above :)

Anyway - SML/NJ accepts both:

val _ = let val x = ref nil in () end

val _ = let fun f (a : 'a) (b : 'b) = b  val x = f nil in () end

Is this because SML/NJ allows more programs than it should
or is it because the inference should only "terminate" at
top-level and not at every nested closure point?

In my semantics right now I expect to a complete closure generating
a principal type at every closure point separately
(i.e. every val binding). This only excludes type variables bound
further out (i.e. the "occuring unguarded" thing p. 18-19 in
the Definition of SML'97).

If I don't do this I think I will get some weird limitations
on my extensible records and optional fields
(which is the main point of the language).

Anyway - my spec. goes online sometime late today or tomorrow I think.
I would really like some comments on these issues :)


Cheers
-- 
http://www.HardcoreProcessing.com