[MLton] where and nj-deviations

[Stephen Weeks]

> For example, SML/NJ rejects
> 
> (* E *)
> structure S = struct type t = int end
> signature SIG =
>   sig
>      structure T : sig type t end = S
>   end
>   where type T.t = S.t
> 
> with: "where type defn applied to definitional spec"

Rejecting this program seems reasonable to me (for some notion of
reasonable, given that this isn't SML), since the following SML should
be rejected.

structure S = struct type t = int end
signature SIG =
  sig
     structure T : sig type t = S.t end
  end
  where type T.t = S.t

The reason it should be rejected is that once t has been defined to be
S.t, i.e. int, then a later attempt to define t is really an attempt
to define int, which is nonsensical.  

The reason that SML/NJ gives for rejecting the program is wrong, and
shows up in another case where SML/NJ incorrectly rejects SML programs
such as:

signature S =
   sig
      type t
      type u = t
   end where type u = int;

> SML/NJ also rejects
> 
> (* F *)
> structure S = struct type t = int end
> signature SIG =
>   sig
>     structure T : sig type t end where type t = S.t
>   end
>   where type T.t = S.t
> 
> with: "where type defn applied to definitional spec"

This is correctly rejected, again for the same reason.  Also again,
the reason SML/NJ gives is wrong.

> On the other hand, MLton accepts (* F *).  But, I'm fairly certain that
> that is a bug, because MLton also accepts:
> 
> (* G *)
> structure S = struct type t = int end
> signature SIG =
>   sig
>     structure T : sig type t end where type t = S.t
>   end
>   where type T.t = bool
> 
> which clearly sends conflicting messages about the type of T.t.

You are correct that MLton is wrong to accept these.  My last checkin
fixes this.  Now for both (* F *) and (* G *), MLton reports:

 	type T.t is already defined as int32 and cannot be redefined

There is a similar error when attempting to redefine nonlocal types,
even if they aren't rigid.  For example:

signature SIG =
   sig
      type t
      structure S: sig type u = t end where type u = int
   end

leads to the error:

	type u is not local and cannot be redefined

Slightly more interesting:

signature SIG =
   sig
      type t
      structure S: sig type u = t end where type u = t * t
   end

leads to the same error with MLton.  Amusingly enough, that signature
causes Poly/ML to diverge.

> However, SML/NJ accepts
> 
> (* H *)
> structure S = struct type t = int end
> signature SIG =
>   sig
>     structure T : sig type t end where type t = S.t
>   end
>   where T = S
> 
> which is arguably equivalent to (* F *) when one expands "where T = S"
> by the equivalence of (* A *).  But, SML/NJ rejects (* F *) and accepts
> (* H *). 

I agree that I would expect (* H *) to be rejected.

> There may also be a bug in SML/NJ, because it accepts
> 
> (* I *)
> structure R = struct type t = bool end
> structure S = struct type t = int end
> signature SIG =
>   sig
>     structure T : sig type t end where type t = S.t
>   end
>   where T = R
> 
> which, like (* G *) seems to be claiming conflicting things about the type
> of T.t.

Agreed, this should be rejected because the T = R is really trying to
define int to be bool.

> In any case, I'm not sure whether SML/NJ's definitional structure
> specifications can really be replicated with where and/or where type
> constraints. 

Who knows.  If there were a spec we could at least think about it.
But there isn't, and things look very inconsistent in SML/NJ.  I am
content to save my time and leave it at that.

> (The analogy would seem to be that one cannot always replace
> a definitional type specification with a where type constraint.) 

I don't understand this statement.  Definitional type specifications
are syntactic sugar for where types (page 59)

	type t = u
	--->
	include sig type t end where type t = u

> The problem would seem that the "real" equivalent of (* C *) is
>
> (* J *)
> structure S = struct type t = int end
> signature SIG =
>   sig
>     structure T : sig type t = S.t end
>   end
> 
> The "problem" with that is that if instead of (* C *) we started with:
> 
> (* K *)
> signature T = sig type t end
> structure S = struct type t = int end
> signature SIG =
>   sig
>     structure T : T = S
>   end
> 
> then we still need to expand to (* J *), which requires replicating the T
> signature in order to push the definitional specification to the type.

I didn't follow this bit.  But I'm not sure it matters.  If you think
it does, please re-explain.


In any case, other than the Elsman bug documented in the user guide,
I think signature elaboration in MLton is now much more solid.  Keep
those bug reports coming.