[MLton] signature language lacking

[Matthew Fluet]

On Wed, 13 Feb 2008, Vesa Karvonen wrote:
> On Feb 13, 2008 6:47 AM, Henry Cejtin <henry.cejtin at sbcglobal.net> wrote:
>> Consider the following piece of SML code:
> [...]
>>         structure S: sig
>>            structure A: sig
>>               type t = S.at
>>               val f: S.at -> S.bt
>>            end
>>            structure B: sig
>>               type t = S.bt
>>               val f: S.bt -> S.at
>>            end
>>         end = S
>>
>> Unless I am confused, the result is a structure S which has nothing in it but
>> two sub-structures.  Each of these two sub-structures has only a single  type
>> and a single function in it.  The two types are completely opaque except that
>> the two functions map between them.

The two types are opaque (in representation), but do have identities and 
are manifestly equal to the (now shadowed) types in the original S 
structure.

My point is that the abstraction/hiding idioms that one can express with 
scoping and shadowing of identifiers are separate from the idioms that one 
can express with just signature matching.  (I think.)  Though, it would be 
nice to be able to express the signature without resorting to 
shadowing/scoping the original S signature.

Standard ML has the additional oddity that you can only declare signatures 
at the top-level (not within a local .. in .. end), so you can't even 
apply some of the scoping/shadowing idioms to the signature decl.

>> My question is: is there any way to specify  a  signature  such  that  opaque
>> matching  to that signature would express exactly this? [...]
>
> I think you are quite right and the signature language is too weak to
> express the desired signature.  Specifically, there is no way to refer
> to (i.e. write the path to) the type defined in the second
> substructure from the first substructure signature.

I agree.  I think Vesa's suggestion with the sharing constraints are a 
fairly natural solution; MLton uses them for the various ILs with exp/decl 
recursion.