[MLton] Question about Definition of SML :)

[Anoq of the Sun]

Stephen Weeks wrote:
> Actually, I implemented the new front end.

OK - sorry, I have misunderstood that then :)

> Consequently, MLton and SML/NJ incorrectly accept
> expressions like the following.
> 
>    let
>       datatype A = C of bool -> bool
>    in
>       fn C x => x true
>    end
> 
> There is no soundness reason for rejecting this expression -- it is
> rejected only due to an artefact of how type generativity is
> "implemented" in the definition.  Personally, I think the definition
> should have been written to explicitly maintain type name sets and
> more directly enforce generativity, which would allow the above.

OK. The reason I'm asking these things is that I'm writing another
language specification. I also maintain type names explicitly.
Mostly because I think the circle-plus-thing is a little too
indirect (even though of course it doesn't clutter up the
readability). So far I'm actually going for a scheme where
I don't allow redeclaring a datatype with the same name
(in the source-code that is) at all.

> In practice, I don't know how much it matters.  I've never heard of
> any examples where someone was porting code from SML/NJ to another
> compiler and ran into the restriction.  I'd be interested to hear of
> any.
> 
> If pressed, I could probably figure out a way to add the side
> condition to MLton.

Thanks a lot - but I don't have any problems with it :)
Don't change anything for my sake.

> > As far as I can see, the restriction:
> >
> > tynames VE \subseteq T of C
> >
> > in rule (14) p. 23 does the same to ensure that
> > one doesn't unpack an exception with a datatype
> > value which was raised out of scope from where
> > it was declared.
> 
> As far as I know, this side condition and the one on rule 26 are
> completely unnecessary from a soundness point of view.  That is, all
> the programs they cause to be rejected will run without "going wrong"
> in the type soundness sense.  Could you please explain if you have an
> example for 14 that shows otherwise.

Actually, I think I was also mistaken before. What I was thinking of was
something like:

let
  datatype T = C
  exception E of T
in
  raise E C
end
  handle E x => x

But actually it would not even be possible to have this handler using E
(or at least it would not be the same E but an exception declared elsewhere
and then it would never catch any exception in the first place).
But if you say that these rules are also to ensure that new names are
generated then maybe another declared E would catch the one from the
nested declaration - which would clearly be a problem.

> Only the ML Kit of all the SML implementations
> rejects the following program as required by the side condition on
> rule 14.
> 
> val _ =
>    let
>       val x = ref []
>       datatype a = B
>       val _ = x := [B]
>    in
>       ()
>    end

Ouch! Adding references and exceptions really has some consequences that
are hard to see. But actually this program should be rejected
just because of

val x = ref []

This violates the value-restriction. On p. 19 the constructor ref is
excluded from the allowed constructors of Non-expansive expressions.

> I agree with you that the side condition on rule 26 is redundant, but
> only due to a subtle point (possibly a mistake).  If the C + VE on the
> top had been written with a circled plus instead of a plain plus, then
> the side condition would not be redundant. 

Adding a circle plus would be a little confusing here I think. The
circle plus adds type names and the side condition restricts it.
Knowing how these rules would take precedence over one another
would be a tricky issue.

> With a circle plus, the
> context used to elaborate the valbind could include type names defined
> by the valbind, so if the side condition weren't there then the
> following program would be accepted.
> 
> val rec f =
>    fn x =>
>    let
>       datatype A = C of bool -> bool
>    in
>       fn C x => x true
>    end
> 
> There are two ways to correct the rule: remove the side condition, or
> change the circle to a circle-plus.

OK - that for sure is very subtle. This means that the recursive circle
plus would even override the condition in rule (4).

I think I'm beginning to get to the point where I will just
choose the simplest possible solutions in my language to avoid
many of these issues altogether :)

I definately think that I'm not in favour of using something like 
circle plus in rule (26). Thus I wouldn't need the side-condition either.

Anyway - thanks a lot for all the explanations and links! I will
read the articles you gave links to.

I will also try to make my specification available for some public
feedback (maybe around the end of this week) before I hand it in.
It's my bachelor's project and I'll hand it in dec. 19.
Probably a very hard project compared to common bachelor's projects ;)


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