[MLton] Question about Definition of SML :)

[Stephen Weeks]

> I like the point that Andreas made in the discussion you sent the
> link to - about having a simple local rule to reject invalid
> declarations.

Actually that was my point :-) (and Andreas didn't like it).  I can't
quite see how I would formalize such a rule in the definition, though.

> It is what I intend to do in the semantics I have now. But I can see
> that I probably need to explicitly state the requirement that each
> val declaration must give a principal type scheme.  I thought that
> this was what was implied in taking the closure though.

Will you accept or reject

	val x = ref nil

If you reject this based on some local rule, you must presumably also
reject

	val x = ref nil
	val _ = 1 :: !x

and

        val _ =
           let
              val x = ref nil
              val _ = 1 :: !x
           in
              ()
           end


> I don't like that the sequence of declarations at top-level would
> behave differently than at nested let-expressions actually. 

It sounds nice in principle, but in practice the problem is that a
top-level declaration has an open-ended scope including the rest of
the program.  If you accept "val x = ref nil" followed by "val _ = 1
:: !x" in a let declaration and you want to then also accept it at the
top level, it means you may have to look at an arbitrarily large piece
of the program (possibly across module decarations and files) in order
to assign "int list ref" to x.

> Also I can't see that allowing these few extra programs would really
> be any benefit. There are so many other places where ML requires one
> to make an explicit type constraint already.

Maybe.  I tend not to mind type constraintgs too.  I agree it would
certainly be an interesting experiment to have a more constrained rule
and see what happens.  Perhaps you would like to write one in MLton
and try some real programs to see how many break?

> 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 :) 

I mean to say that this program must be accepted.  And in fact all
implementations accept it.  And I have never heard an argument that it
may be rejected.

> 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?

These are both easy to accept, because no type variables make it to
the top level.  SML/NJ assigns new monotypes to free type variables,
and so would accept these at the top level as well, but the new
monotypes would be unusable.