[MLton] Question about Definition of SML :)

[Anoq of the Sun]

Regarding the issue with ref earlier:


Anoq of the Sun wrote:
> Stephen wrote:
> > val _ =
> > >    let
> > >       val x = ref []
> > >       datatype a = B
> > >       val _ = x := [B]
> > >    in
> > >       ()
> > >    end
> 
> > > val x = ref []
> > >
> > > This violates the value-restriction.
> >
> > No.  Without the side condition on rule 14, x can be assigned the
> > monotype "a list ref", so the value restriction does not come in to
> > play.
> 
> I can see now that this is because of the nested val. Writing
> 
> val x = ref []
> 
> alone fails in SML/NJ due to value-restriction.
> but writing
> 
> val _ = let val x = ref [] in () end;
> 
> Is OK.
> 
> So assuming that the SML/NJ behaviour is correct,
> I can't see why this is OK though?
> I thought I understood the scoping rules for type variables
> but I can't see what's happening here. Can you explain this? :)

I have just spoken with Fritz Henglein about this.
He also agrees that

val x = ref nil

violates the value-restriction. So it would appear that
SML/NJ allows more programs than what the Definition of
SML '97 does. 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?


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