[MLton] withtype in signature?

[Matthew Fluet]

>>> Why is 'withtype' not allowed in signatures? The standard?
>>> 
>> Correct.  The grammar of the Definition does not admit "withtype" in 
>> signatures.
>> 
>
> Do you know why they've done that?
> It seems like *more* work to forbid withtype in (only) sig context.

The consensus seems to be that it was an oversight in the Definition.

>> That is one recourse.  Another, almost as verbose means is to define a 
>> structure with exactly the datatype of interest and then bind to that in 
>> the signature:
>> 
>> structure T = struct
>>   datatype test = A of foo * baz | B
>>   withtype foo = string * test
>>   and baz = int
>> end
>> 
>> signature S = sig
>>   datatype test = datatype T.test
>>   type foo = T.foo
>>   type baz = T.baz
>> end
>> 
>
> For my situation, that's almost an improvement...
> However, since datatypes are generative, I have to
> use exactly T's datatype in a matching structure..?
>
> structure Foo : S =
>  struct
>    datatype test = A of foo * baz | B
>    withtype foo = string * test
>    and baz = int
>  end
> won't work. I need to 'open T', right? That's unpleasant.

Correct.  Essentially, T becomes the (one and only) defining occurrence 
of the datatype and types.  Every other occurrence need to be a 
replication.  You don't necessarily need 'open T', you can get by with:

structure Foo : S =
   struct
     datatype test = datatype T.test
     type foo = T.foo
     type baz = T.baz
   end

And, elsewhere in the program, Foo.A will behave correctly.

> I never proposed to extend SML! :-) I just wanted to know if this was
> a bug and/or the reasoning for it, if not a bug. What I am hoping is that
> the standard ruled it out because it was unnecessary in a way I just don't
> see yet. Ideas?

I think, historically, the Definition was formalized before people had 
experience with using its module system in practice.  Certainly, the 
authors were well-versed in the theory of module systems.  But, the 
examples one comes up with for the purposes of a paper are often very 
different than the ones that come up in a large-scale application.