[MLton] Question about Definition of SML :)

[Stephen Weeks]

> I have just spoken with Fritz Henglein about this.  He also agrees
> that
>
> val x = ref nil
>
> violates the value-restriction. 

I disagree.  Even if that is the entire program.  Even if the program
is 

        val x = ref []
        val _ = 1 :: !x

> The way I would explain iwhy it's illegal:
>
> nil is a constructor with the type-scheme \/'a.'a list.  By rule (2)
> this generalizes some type \tau which then becomes 'a list with 'a
> being free - i.e. a meta-variable (if my understanding of
> "generalizing a type is correct?").  The inference continues up to
> the val binding where the closure is taken - thus capturing the 'a
> to bind it again.  But capturing an 'a during closure here is
> illegal due to the restriction p. 19-20 about closure since the
> expression 'ref nil' contains an application with the constructor
> ref which makes the expression expansive according to the definition
> of expansive p. 19.
>
> Did I understand it correctly?

Your understanding of all of the rules individually seems fine to me.
The issue is that you are missing the big picture, which is that you
are (correctly) only arguing why a *particular* elaboration can not
succeed.  And I agree with you.  What you are not arguing (and
couldn't possibly argue, because it isn't true) is that all
elaborations can not succeed.  For example, it is perfectly valid to
elaborate the program

        val x = ref []

assigning x the type "int list ref", or "unit list ref", or any other
monotype.  That does not violate the value restriction, because it
does not assign x a type scheme.

As I said earlier, the Definition requires the elaborator to find an
elaboration if one exists (see the end of G.8).  If it didn't do this,
it would be perfectly legal for the elaborator to reject all programs.

For more discussion of this point, and other value restriction stuff,
see

        http://groups.google.com/groups?hl=en&lr=&ie=UTF-8&oe=UTF-8&threadm=9m6h85%24fk9%241%40cantaloupe.srv.cs.cmu.edu&rnum=1&prev=/groups%3Fq%3Dvalue%2Brestriction%2Bgroup:comp.lang.ml%2Bauthor:Andreas%2Bauthor:Rossberg%26hl%3Den%26lr%3D%26ie%3DUTF-8%26oe%3DUTF-8%26selm%3D9m6h85%2524fk9%25241%2540cantaloupe.srv.cs.cmu.edu%26rnum%3D1

I made a concious decision when building the MLton elaborator that
MLton would not instantiate unspecified top-level types with
monotypes, because of the potential confusion that would result.  This
seems in accordance with another comment at the end of G.8.  Hence,
MLton rejects

        val x = ref nil

reporting "unable to infer type for x".

However, I also made a concious decision that MLton would use as much
context as allowed by the definition to try to determine types.  Hence
MLton accepts

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

Because the Definition does not allow the context to extend beyond
structure-level declarations (see right before E.1 on page 71), MLton
rejects

        val x = ref nil
        signature S = sig end
        val _ = 1 :: !x

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