[MLton] Question about Definition of SML :)

[Stephen Weeks]

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

I don't see how exceptions can cause problems with this stuff, since
exception declarations don't generate new type names, they just add
new variants to the exn datatype.  The rules in the dynamic semantics
that allocate new exception names (dynamically) prevent exceptions
from going wrong.

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

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

There is no issue of precedence.  The rules define a collection of
relations inductively.  The Definition requires that if there is some
elaboration that succeeds (i.e. element of the relation), then the
type inference must find it.

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

If you change the circle to circle-plus, then one could make the type
name for A avaiable when elaborating "fn x => ...", but then the side
condition on (26) would rule out the elaboration of the "rec f =
..." because the type name for A would be in VE but not in T of C.

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

Sounds good.

> Probably a very hard project compared to common bachelor's projects ;)

Indeed.