Re: [Sml-implementers] Free type variables on toplevel

[Andreas R. <ros...@ps...>]

"Derek R. Dreyer" wrote:
> 
> At first glance, these
> two examples might appear to elaborate the same way, but I claim that according
> to the Definition it's not clear that they need to.

Right. Program 1 definitely has to elaborate (although it does not on
some of the systems I tried, namely SML/NJ). I was considering examples
like program 2.

> In Program 2, however, the two val's are in different topdec's.  A careful
> reading of Section 8 on the semantics of Programs seems to indicate that there
> are two possible outcomes for the elaboration and execution of Program 2.  Under
> Rule 188, we could guess the type of x as being "bool list" as in Program 1, and
> thus elaborate the second val binding fine.  However, it is also possible to
> guess the type of x as being "int list". In this case, when we get around to
> elaborating the second val binding, it will fail to elaborate.  This is ok
> because this causes Rule 187 to apply, resulting in the abortion of execution of
> the second val binding.  The ambiguity is due to the negative premise of Rule
> 187, which is matched when a topdec does *not* elaborate.  It is rather
> concerning that there is such an ambiguity, so either I'm wrong about Rule 187
> applying or the Definers could maybe comment on this?

I believe this is not a valid interpretation of rule 187. For most
programs, there are arbitrary many non-elaborations, AFAICS. Thus, if
the rule would have the meaning you suggest, it would follow that almost
all programs could be legally rejected by an implementation.

So I think that the correct interpretation of the negative premise is:
there does not exist any elaboration (if I understand correctly, your
interpretation would be: there exists a non-elaboration).

> 3) A related issue that I observed while playing around was that NJ and Moscow
> have very different behavior with respect to failed elaborations in general, and
> as usual Moscow ML is the one that is in line with the Definition.  The specific
> question is: When you hit a topdec that does not elaborate, do you stop or do
> you keep elaborating and executing the program?  The Definition (rule 187 as
> before) is quite clear on this point: you keep going.  Thus, for instance,
> 
> val x = 3; val y = x + true; val z = 4;
> 
> causes NJ to give an error at the second val binding and stop, not elaborating
> the third one.  Moscow ML, however, gives an error at the second val binding and
> continues, elaborating "val z = 4" and adding z to the environment.  The
> question is: which is really better?  Although I appreciate that Moscow ML
> implements the Definition faithfully, I sort of think NJ is right: it makes more
> sense for the compiler to stop evaluating the program once it hits a type
> error.

The program rules mainly describe the behaviour of the interactive
toplevel. For this, it is of course important that the user can continue
yping and executing programs after encounter of an erroneous input.
Everybody seems to agree that this focus on an interactive toplevel is
an anachronism, though.

Best regards,

	- Andreas