[MLton] Question about Definition of SML :)
Anoq of the Sun
anoq@HardcoreProcessing.com
Thu, 04 Dec 2003 17:40:59 +0200
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